<br><div class="gmail_extra"><br><br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<br>
I propose to not use ∶ in the special syntax for Σ. Sure, it is intended<br>
to be similar to :. However, I think this similarity is precisely its<br>
weakness. You cannot tell from looking at the code whether your code is<br>
syntactically correct or not. Furthermore, there is a semantic problem.<br>
The symbol ∶ is called RATIO, but Σ does not have anything to do with<br>
ratios. I propose to use an alternative syntax, maybe the following:<br>
<br>
    syntax Σ A (λ x → B) = Σ[ x ∈ A ] B</blockquote><div><br></div><div>for the record (ha!) my original proposal was to have another variant of syntax like so:</div><div><br></div><div><div>syntax ∃ (\(_:A) → B) = A × B</div>
</div><div><br></div><div>adding the following forms to the concrete syntax (meaning after the ==&gt;)</div><div><br></div><div>(x : A) × B ==&gt; ∃ (λ (x : A) → B)</div><div>A × B ==&gt;  ∃ (λ (_ : A) → B)<br></div><div>
<br></div><div>(the binders x : A use the regular syntax)</div><div><br></div><div>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.</div>
<div>  </div><div>Cheers,</div><div>JP.</div></div></div>