The fast_instance% term elaborator

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.

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.

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.