[Agda] : vs. ∶

[Wolfram Kahl]

On Wed, Nov 28, 2012 at 11:12:34PM +0100, 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.

Ouch.

How can I rename or hide this syntax while still importing Σ ?
(As far as I know, ``syntax'' is only automatically imported with the
 underlying identifier, and cannot be named in import lists?)


Wolfram