Lean Reference Manual - `structure` syntax

Stream: new members

[Rajiv]

I am trying to get a better intuition for structure syntax in Lean.

In Lean Reference Manual, Section 4.9, https://leanprover.github.io/reference/declarations.html#structures-and-records following is mentioned.

structure foo (a : α) extends bar, baz : Sort u :=
constructor :: (field₁ : β₁) ... (fieldₙ : βₙ)

Along with scheme for a single single constructor.

foo.constructor : Π (a : α) (_to_foo : foo) (_to_bar : bar)
  (field₁ : β₁) ... (fieldₙ : βₙ), foo a

I was wondering if _to_foo : foo should be _to_baz : baz or is there some reason why the constructor is taking in a term of foo?

[Alex J. Best]

Yeah that looks like a typo, checking the followiing in lean

variable {α: Type*}
universe u
structure bar (a : α) : Sort* :=
constructora :: (field₁ : α)
structure baz (a : α) : Sort* :=
constructors :: (field₂ : α)
structure foo {a : α} extends bar α , baz α  : Sort*:=
constructor :: (field₁l : α) (fieldₙ : α)
#print prefix foo

we see that foo.constructor takes a bar and a baz.

[Alex J. Best]

Maybe

variable {α: Type*}
universe u
structure bar : Type (u+1) :=
constructora :: (field₁ : Type u)
structure baz : Type (u+1) :=
constructors :: (field₂ : Type u)
structure foo {a : α} extends bar , baz :=
constructor :: (field₁l : field₂) (fieldₙ : field₁)
#print prefix foo

makes it look more like the constructor there

[Rajiv]

Thanks Alex.