leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 47 forks source link

Explanation of what a structure is #122

Closed hrmacbeth closed 3 hours ago

hrmacbeth commented 5 hours ago

The introduction to the chapter on structures says,

Remember that a non-recursive inductive type that contains only one constructor is called a structure or record.

This appears to need further qualification. Consider the following, which cannot be expressed as a structure:

variable (α β : Type) (f : β → α → α)

inductive Foo : α → α → Prop
  | bar (b : β) (a : α) : Foo a (f b a)

Zulip discussion

hrmacbeth commented 3 hours ago

Oops, didn't realise this was the Lean 3 repo. Reopened at https://github.com/leanprover/theorem_proving_in_lean4/issues/137.