[Agda] : vs. ∶

[Martin Escardo]

I define

record Σ {X : Set} (Y : X → Set) : Set where
  constructor _,_
  field
   π₀ : X
   π₁ : Y π₀

instead. So you have to write Σ {X} Y rather than Σ X Y. On the other 
hand, you can write Σ \(x : X) → Y x, or even Σ \x → Y x when X can be 
inferred. But this would break existing code that uses the libraries.

The ideal solution, however, would be so add Σ, Π, and ∃ as primitive, 
as was done with ∀, so that one can write Σ(x : X) → Y x, or Σ x → Y x.

Martin

On 04/05/12 16:09, Wolfgang Jeltsch wrote:
> Hello,
>
> 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
>
> What do others think?
>
> Best wishes,
> Wolfgang
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda