Instance (Lean)

Definition

Instance ( Lean)

An instance is a term supplying the data or proofs required by a typeclass, made available to Lean’s instance synthesis. For a class and parameter , an instance has type

Instances are commonly registered with instance. An instance-implicit binder [i : C α] or a local declaration letI : C α := value makes a term available within its scope. Merely defining a term of class type does not register it for search.

An instance may itself have parameters and require other instances; it need not be an implementation for a single concrete type.