[Agda] binder for existential quantifier

[Bengt Nordstrom]

Sorry Nisse, but this kind of lexical nonsense is a very efficient way
to keep Agda away from new users!

Agda is based on very good ideas and these should not be shadowed by
Unicode hackery!

All the best,
Bengt

On Fri, Apr 8, 2011 at 3:46 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-04-08 13:02, Jean-Philippe Bernardy wrote:
>> syntax Σ A (λ x → B) = Σ[ x ∶ A ] B
>
> Note that the character which may look like a colon is /not/ the ASCII
> colon character, it is U+2236 (RATIO). If you are using the Agda input
> method, then you can insert this character by typing \:.
>
> --
> /NAD
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>