Re: [Agda] : vs. :

Altenkirch Thorsten psztxa at
Tue Dec 4 11:15:57 CET 2012

I agree that it is a good idea to avoid having symbols which look the same
(like ∶ and :).

I think that it should be left to the maintainer of the library to choose
the symbol and I think ∈ is a good choice. I suggest that we finish this


On 04/12/2012 10:10, "Nils Anders Danielsson" <nad at> wrote:

>On 2012-11-29 16:51, Wolfgang Jeltsch wrote:
>> RATIO is for ratios. Type membership is completely different from
>> ratios. So the choice of RATIO is just plain wrong.
>I don't care too much about this. I suspect that many symbols are used
>in the "wrong" way. For instance, what does λ have to do with taking an
>argument? As another example, I mostly use - rather than − (minus) or ‐
>(hyphen), and Agda uses white space (f x) rather than the function
>application character (f⁡x).
>> In addition, we have the confusion between ∶ and : (which can cause a
>> lot of pain, especially to newcomers).
>I think this is more serious. I've been bitten by this myself. I don't
>plan to revert to the use of ∶, but I'm not wedded to the names/syntaxes
>_∋_ and Σ[_∈_]_.
>Agda mailing list
>Agda at

More information about the Agda mailing list