[Agda] : vs. ∶

Martin Escardo m.escardo at cs.bham.ac.uk
Fri May 4 17:37:39 CEST 2012

I define

record Σ {X : Set} (Y : X → Set) : Set where
  constructor _,_
   π₀ : 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.


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

More information about the Agda mailing list