Structure (Lean)

Definition

Structure (Lean)

A structure in Lean is a record type declared with structure, grouping named fields into one value. Fields may contain data, functions or proofs. The declaration generates a constructor for assembling the fields and projections for accessing them, written value.field.

A structure type may depend on parameters, and later fields may depend on earlier fields. Declaring it with class additionally registers the type as a typeclass; an ordinary structure declaration does not enable instance synthesis by itself.