Zulip Chat Archive

Stream: new members

Topic: Lean Reference Manual - `structure` syntax


Rajiv (Dec 10 2020 at 12:45):

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 (Dec 10 2020 at 13:25):

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 (Dec 10 2020 at 13:29):

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 (Dec 10 2020 at 13:32):

Thanks Alex.


Last updated: Dec 20 2023 at 11:08 UTC