[Agda] binder for existential quantifier

Nils Anders Danielsson nad at chalmers.se
Fri Apr 8 15:46:16 CEST 2011


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



More information about the Agda mailing list