def Lean.Meta.getCtorNumPropFields (ctorInfo : ConstructorVal) : MetaM Nat

inductive Lean.Meta.InjectionResultCore : Type

• solved : InjectionResultCore
• subgoal (mvarId : MVarId) (numNewEqs : Nat) : InjectionResultCore

def Lean.Meta.injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCore

inductive Lean.Meta.InjectionResult : Type

• solved : InjectionResult
• subgoal (mvarId : MVarId) (newEqs : Array FVarId) (remainingNames : List Name) : InjectionResult

def Lean.Meta.injectionIntro (mvarId : MVarId) (numEqs : Nat) (newNames : List Name) (tryToClear : Bool := true) : MetaM InjectionResult

def Lean.Meta.injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) : MetaM InjectionResult

inductive Lean.Meta.InjectionsResult : Type

• solved : InjectionsResult

  injections closed the input goal.

• subgoal (mvarId : MVarId) (remainingNames : List Name) (forbidden : FVarIdSet) : InjectionsResult

  injections produces a new goal mvarId. remainingNames contains the user-facing names that have not been used. forbidden contains all local declarations to which injection has been applied. Recall that some of these declarations may not have been eliminated from the local context due to forward dependencies, and we use forbidden to avoid non-termination when using injections in a loop.

def Lean.Meta.injections (mvarId : MVarId) (newNames : List Name := []) (maxDepth : Nat := 5) (forbidden : FVarIdSet := ∅) : MetaM InjectionsResult

Applies injection to local declarations in mvarId. It uses newNames to name the new local declarations. maxDepth is the maximum recursion depth. Only local declarations that are not in forbidden are considered. Recall that some of local declarations may not have been eliminated from the local context due to forward dependencies, and we use forbidden to avoid non-termination when using injections in a loop.