Typeclass (Lean)

Definition

Typeclass ( Lean)

A typeclass is a type registered with Lean’s instance synthesis. A parameterised class specifies data, operations or propositions required for its parameters; a term supplies them for .

A declaration using an instance-implicit parameter [C α] asks Lean to find a suitable instance automatically when that argument is omitted. Classes are commonly declared with class, which defines a structure and registers it as a class.