Re: [Agda] : vs. ：

[Altenkirch Thorsten]

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
discussion.

Thorsten
 


On 04/12/2012 10:10, "Nils Anders Danielsson" <nad at chalmers.se> 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 Σ[_∈_]_.
>
>-- 
>/NAD
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda