structure Lean.Meta.InductionSubgoal : Type

• mvarId : MVarId
• fields : Array Expr
• subst : FVarSubst

instance Lean.Meta.instInhabitedInductionSubgoal : Inhabited InductionSubgoal

structure Lean.Meta.AltVarNames : Type

• explicit : Bool
• varNames : List Name

instance Lean.Meta.instInhabitedAltVarNames : Inhabited AltVarNames

def Lean.Meta.getMajorTypeIndices (mvarId : MVarId) (tacticName : Name) (recursorInfo : RecursorInfo) (majorType : Expr) : MetaM (Array Expr)

Auxiliary method for implementing induction-like tactics. It retrieves indices from majorType using recursorInfo. Remark: mvarId and tacticName are used to generate error messages.

def Lean.Meta.mkRecursorAppPrefix (mvarId : MVarId) (tacticName : Name) (majorFVarId : FVarId) (recursorInfo : RecursorInfo) (indices : Array Expr) : MetaM Expr

Auxiliary method for implementing induction-like tactics. It creates the prefix of a recursor application up-to motive. The motive is computed by abstracting major and indices at mvarId.getType. It retrieves indices from majorType using recursorInfo. Remark: mvarId and tacticName are used to generate error messages.

def Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array Meta.AltVarNames := #[]) : MetaM (Array Meta.InductionSubgoal)