Lean.Meta.Tactic.AuxLemma

Type

Equations

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

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

Equations

Lean.Meta.mkAuxLemma levelParams type value = do let env ← Lean.getEnv let s ← pure (Lean.EnvExtension.getState Lean.Meta.auxLemmasExt env) let mkNewAuxLemma : Lean.MetaM Lean.Name := let auxName := Lean.Name.mkNum (Lean.Environment.mainModule env ++ `_auxLemma) s.idx; do Lean.addDecl (Lean.Declaration.thmDecl { toConstantVal := { name := auxName, levelParams := levelParams, type := type }, value := value }) Lean.modifyEnv fun env => Lean.EnvExtension.modifyState Lean.Meta.auxLemmasExt env fun x => match x with | { idx := idx, lemmas := lemmas } => { idx := idx + 1, lemmas := Std.PersistentHashMap.insert lemmas type (auxName, levelParams) } pure auxName match Std.PersistentHashMap.find? s.lemmas type with | some (name, levelParams') => if (levelParams == levelParams') = true then pure name else mkNewAuxLemma | none => mkNewAuxLemma