[Agda] : vs. ∶

Wolfgang Jeltsch g9ks157k at acme.softbase.org
Thu Nov 29 16:47:56 CET 2012


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



More information about the Agda mailing list