structure Lean.Meta.AuxLemmas : Type

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

Instances For

• Lean.Meta.instInhabitedAuxLemmas

instance Lean.Meta.instInhabitedAuxLemmas : Inhabited AuxLemmas

Equations

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

opaque Lean.Meta.auxLemmasExt : EnvExtension AuxLemmas

def Lean.Meta.mkAuxLemma (levelParams : List Name) (type value : Expr) (prefix? : Option Name := none) (cache : Bool := true) : MetaM 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 environment branch. For expensive auxiliary lemmas that should be deduplicated even across different environment branches, consider using realizeConst instead.

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.