[Agda] : vs. ∶

Wolfgang Jeltsch g9ks157k at acme.softbase.org
Fri May 4 17:09:18 CEST 2012


I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
to be similar to :. However, I think this similarity is precisely its
weakness. You cannot tell from looking at the code whether your code is
syntactically correct or not. Furthermore, there is a semantic problem.
The symbol ∶ is called RATIO, but Σ does not have anything to do with
ratios. I propose to use an alternative syntax, maybe the following:

    syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

What do others think?

Best wishes,

More information about the Agda mailing list