The fast_instance% and inferInstanceAs% term elaborators

def Mathlib.Elab.FastInstance.fastInstance : Lean.ParserDescr

fast_instance% inst takes an expression for a typeclass instance inst, and unfolds it into constructor applications that leverage existing instances. It uses the expected type to fill in the constructor applications and lambda binders of data fields.

For instance, when used as

instance instSemiring : Semiring X := sorry
instance instRing : Ring X := fast_instance% Function.Injective.ring ..

this will define instRing as a nested constructor application that refers to instSemiring rather than applications of Function.Injective.ring or other non-canonical constructors. The advantage is then that instRing.toSemiring unifies almost immediately with instSemiring, rather than having to break it down into smaller pieces.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Elab.FastInstance.elabFastInstance : Lean.Elab.Term.TermElab

fast_instance% inst takes an expression for a typeclass instance inst, and unfolds it into constructor applications that leverage existing instances. It uses the expected type to fill in the constructor applications and lambda binders of data fields.

For instance, when used as

instance instSemiring : Semiring X := sorry
instance instRing : Ring X := fast_instance% Function.Injective.ring ..

this will define instRing as a nested constructor application that refers to instSemiring rather than applications of Function.Injective.ring or other non-canonical constructors. The advantage is then that instRing.toSemiring unifies almost immediately with instSemiring, rather than having to break it down into smaller pieces.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Elab.FastInstance.«termInferInstanceAs%_» : Lean.ParserDescr

inferInstanceAs% A is shorthand for fast_instance% inferInstanceAs A. This is preferred over inferInstanceAs when the instance can be reduced to constructor applications. In that case, the parameters of the constructors will be filled in using the expected type, so that the instance will unfold nicely during unification.

Equations

• One or more equations did not get rendered due to their size.