[Agda] : vs. ∶

[Nils Anders Danielsson]

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