Explanation of what a structure is

[hrmacbeth]

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