Documentation

Lean.Meta.Tactic.Injection

source
def Lean.Meta.getCtorNumPropFields (ctorInfo : Lean.ConstructorVal) :
Lean.MetaM Nat
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Meta.InjectionResultCore:
Type
source
def Lean.Meta.injectionCore (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
Lean.MetaM Lean.Meta.InjectionResultCore
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Meta.InjectionResult:
Type
source
def Lean.Meta.injectionIntro (mvarId : Lean.MVarId) (numEqs : Nat) (newNames : List Lean.Name) (tryToClear : optParam Bool true) :
Lean.MetaM Lean.Meta.InjectionResult
Equations
source
def Lean.Meta.injectionIntro.go (tryToClear : optParam Bool true) :
Nat → Lean.MVarId → Array Lean.FVarId → List Lean.Name → Lean.MetaM Lean.Meta.InjectionResult
Equations
source
def Lean.Meta.injection (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (newNames : optParam (List Lean.Name) []) :
Lean.MetaM Lean.Meta.InjectionResult
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.injections (mvarId : Lean.MVarId) (maxDepth : optParam Nat 5) :
Lean.MetaM (Option Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.injections.go (mvarId : Lean.MVarId) :
Nat → List Lean.FVarId → Lean.MVarId → Lean.MetaM (Option Lean.MVarId)