[Agda] : vs. ∶

[Wolfgang Jeltsch]

Am Mittwoch, den 28.11.2012, 21:22 -0500 schrieb Andreas Abel:
> On 28.11.12 5:12 PM, Nils Anders Danielsson wrote:
> > On 2012-05-04 17:09, Wolfgang Jeltsch wrote:
> >> I propose to use an alternative syntax, maybe the following:
> >>
> >>      syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
> >
> > I switched to this syntax. I also renamed Function.type-signature to
> > _∋_, and removed the "x ∶ A" syntax for it.
> 
> Mmh, don't know.  With unicode, there is always the confusion issue, 
> like with :: and \:: and the like.

So I think we should not add to this confusion by using symbols that
look like the ones we want, but whose actual meanings as per the Unicode
standard are different from what we want.

Best wishes,
Wolfgang