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

Equations

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

inductive Lean.Meta.InjectionResultCore : Type

• solved : Lean.Meta.InjectionResultCore
• subgoal (mvarId : Lean.MVarId) (numNewEqs : Nat) : Lean.Meta.InjectionResultCore

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.

inductive Lean.Meta.InjectionResult : Type

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

def Lean.Meta.injectionIntro (mvarId : Lean.MVarId) (numEqs : Nat) (newNames : List Lean.Name) (tryToClear : Bool := true) : Lean.MetaM Lean.Meta.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 → Lean.MVarId → Array Lean.FVarId → List Lean.Name → Lean.MetaM Lean.Meta.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 : Lean.MVarId) (fvarId : Lean.FVarId) (newNames : List Lean.Name := []) : Lean.MetaM Lean.Meta.InjectionResult

Equations

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

inductive Lean.Meta.InjectionsResult : Type

• solved : Lean.Meta.InjectionsResult

  injections closed the input goal.

• subgoal (mvarId : Lean.MVarId) (remainingNames : List Lean.Name) (forbidden : Lean.FVarIdSet) : Lean.Meta.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 : Lean.MVarId) (newNames : List Lean.Name := []) (maxDepth : Nat := 5) (forbidden : Lean.FVarIdSet := ∅) : Lean.MetaM Lean.Meta.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 Lean.FVarId) (mvarId : Lean.MVarId) (newNames : List Lean.Name) (forbidden : Lean.FVarIdSet) : Lean.MetaM Lean.Meta.InjectionsResult