Re: [Agda] : vs. ∶

[Jean-Philippe Bernardy]

> I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
> to be similar to :. However, I think this similarity is precisely its
> weakness. You cannot tell from looking at the code whether your code is
> syntactically correct or not. Furthermore, there is a semantic problem.
> The symbol ∶ is called RATIO, but Σ does not have anything to do with
> ratios. I propose to use an alternative syntax, maybe the following:
>
>     syntax Σ A (λ x → B) = Σ[ x ∈ A ] B


for the record (ha!) my original proposal was to have another variant of
syntax like so:

syntax ∃ (\(_:A) → B) = A × B

adding the following forms to the concrete syntax (meaning after the ==>)

(x : A) × B ==> ∃ (λ (x : A) → B)
A × B ==>  ∃ (λ (_ : A) → B)

(the binders x : A use the regular syntax)

The implementation was never completed due to motive, means and opportunity
never aligning. A stumbling block is that a binder (x : A) is not in the
same syntactic category as identifier parts. So this requires profound
reworking of the parser.

Cheers,
JP.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121129/4a8f7092/attachment.html