[Agda] : vs. ∶

[Cezar Ionescu]

Nils Anders Danielsson <nad at chalmers.se> wrote:

> On 2012-11-29 03:22, Andreas Abel wrote:
> > I'd prefer the RATIO symbol (fake colon) to the epsilon.
> 
> Any other opinions?

I'm with Andreas on this one.  The (fake) colon is more consistent with
what people know from logic courses, for example classical multi-sorted
predicate logic etc.  It is also more consistent when using existentials
to express properties of functions, because then you have |f : A -> B|
as usual, instead of |f \in A -> B|.  I already spent some time
explaining to some of my colleagues why the set-membership symbol is
misleading in this context, I don't want now to start using it :)

Best,
Cezar.