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

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Meta.InjectionResultCore : Type

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.injectionIntro mvarId numEqs newNames tryToClear = Lean.Meta.injectionIntro.go tryToClear numEqs mvarId #[] newNames

def Lean.Meta.injectionIntro.go (tryToClear : Bool := true) : Nat → MVarId → Array FVarId → List Name → MetaM InjectionResult

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.injectionIntro.go tryToClear 0 x✝² x✝¹ x✝ = pure (Lean.Meta.InjectionResult.subgoal x✝² x✝¹ x✝)

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Meta.injections.go (depth : Nat) (fvarIds : List FVarId) (mvarId : MVarId) (newNames : List Name) (forbidden : FVarIdSet) : MetaM InjectionsResult