[Agda] : vs. ∶

[Wolfram Kahl]

On Thu, Nov 29, 2012 at 11:07:01AM +0100, Nils Anders Danielsson wrote:
> On 2012-11-29 02:30, Wolfram Kahl wrote:
> >(As far as I know, ``syntax'' is only automatically imported with the
> >  underlying identifier, and cannot be named in import lists?)
> 
> That's right.
> 
> >How can I rename or hide this syntax while still importing Σ ?
> 
> I guess you could do something awkward like in the following (untested)
> code:
> 
>   module _ where
> 
>     open import Data.Product hiding (Σ)
> 
>     Σ : ...
>     Σ = Data.Product.Σ

That looks like an option; thanks!

By the way,

  module _ ...

is great! It will save me a lot of dummy name inventing
with corresponding

  open DummyName public

lines --- and first cost me some time
for undoing those I already have...



> I almost never use this syntax

I use it a lot, because I find

  Σ[ x ∶ A ] B

much more readable than

  Σ A (λ x → B)

or

  ∃ (λ x → B)

or

  ∃ (λ (x : A) → B)

.


> I guess I could also introduce a synonym for Σ, and attach
> the syntax to this synonym.

That's probably a reasonable stand-in for enabling separate
import control on syntax rules. Another source of dummy names...


Wolfram