structure Lean.Meta.AuxLemmas : Type

• idx : Nat
• lemmas : Lean.PHashMap Lean.Expr (Lean.Name × List Lean.Name)

instance Lean.Meta.instInhabitedAuxLemmas : Inhabited Lean.Meta.AuxLemmas

Equations

• Lean.Meta.instInhabitedAuxLemmas = { default := { idx := default, lemmas := default } }

opaque Lean.Meta.auxLemmasExt : Lean.EnvExtension Lean.Meta.AuxLemmas

def Lean.Meta.mkAuxLemma (levelParams : List Lean.Name) (type value : Lean.Expr) : Lean.MetaM Lean.Name

Helper method for creating auxiliary lemmas in the environment.

It uses a cache that maps type to declaration name. The cache is not stored in .olean files. It is useful to make sure the same auxiliary lemma is not created over and over again in the same file.

This method is useful for tactics (e.g., simp) that may perform preprocessing steps to lemmas provided by users. For example, simp preprocessor may convert a lemma into multiple ones.

Equations

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