Lean.Meta.Tactic.AuxLemma

source

structure Lean.Meta.AuxLemmas:

Type

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

source

instance Lean.Meta.instInhabitedAuxLemmas:

Inhabited Lean.Meta.AuxLemmas

Equations

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

source

opaque Lean.Meta.auxLemmasExt:

Lean.EnvExtension Lean.Meta.AuxLemmas

source

def Lean.Meta.mkAuxLemma (levelParams : List Lean.Name) (type : Lean.Expr) (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.