[Agda] \exists definition

Daniel Peebles pumpkingod at gmail.com
Wed Aug 22 21:14:52 CEST 2012


If you browse the code in HTML or using the emacs mode, you can
cross-reference everything:

The exists symbol on
http://www.cse.chalmers.se/~nad/listings/lib/Data.Nat.GCD.html#5932 is
actually a hyperlink to
http://www.cse.chalmers.se/~nad/listings/lib/Data.Product.html#608, for
example.

On Wed, Aug 22, 2012 at 3:03 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> On Wed, Aug 22, 2012 at 10:49:37PM +0400, Serge D. Mechveliani wrote:
> > Please,
> > where is the definition for the  \exists  math symbol (type
> constructor?) ?
> > [..]
>
> Sorry, I see it now in  module Data.Product
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120822/7103afe2/attachment.html


More information about the Agda mailing list