[Agda] : vs. ∶

Nils Anders Danielsson nad at chalmers.se
Wed Nov 28 23:12:34 CET 2012


On 2012-05-04 17:09, Wolfgang Jeltsch wrote:
> I propose to use an alternative syntax, maybe the following:
>
>      syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

I switched to this syntax. I also renamed Function.type-signature to
_∋_, and removed the "x ∶ A" syntax for it.

-- 
/NAD



More information about the Agda mailing list