PSigma

Stream: general

[Kind Bubble]

Does anyone know how to set up list notation for PSigma.mk? This gives me errors:

def a : Σ'(x : Unit),Unit  := (Unit.unit, Unit.unit)

I want to be able to make something like this too:

def b : Σ'(x : Unit ),Σ'(x : Unit ),Σ'(x : Unit ),Unit := (Unit.unit, Unit.unit, Unit.unit, Unit.unit)

[Floris van Doorn]

Lean already supports this out of the box, with different brackets:

def a : Σ'(x : Unit),Unit  := ⟨Unit.unit, Unit.unit⟩
def b : Σ'(x : Unit ),Σ'(x : Unit ),Σ'(x : Unit ),Unit := ⟨Unit.unit, Unit.unit, Unit.unit, Unit.unit⟩

[Floris van Doorn]

this called is the anonymous constructor notation, if you want to search for it.

[Eric Wieser]

Are you aware you only need to write the sigma once?

def b : Σ'(x : Unit) (x : Unit) (x : Unit), Unit :=

[Gabriel Ebner]

Are you aware you don't need to write the sigma at all?

def b : (x : Unit) ×' (x : Unit) ×' (x : Unit) ×' Unit :=
  ⟨(), (), (), ()⟩