structure Lean.Meta.InductionSubgoal : Type

• mvarId : Lean.MVarId
• fields : Array Lean.Expr
• subst : Lean.Meta.FVarSubst

instance Lean.Meta.instInhabitedInductionSubgoal : Inhabited Lean.Meta.InductionSubgoal

Equations

• Lean.Meta.instInhabitedInductionSubgoal = { default := { mvarId := default, fields := default, subst := default } }

structure Lean.Meta.AltVarNames : Type

• explicit : Bool
• varNames : List Lean.Name

instance Lean.Meta.instInhabitedAltVarNames : Inhabited Lean.Meta.AltVarNames

Equations

• Lean.Meta.instInhabitedAltVarNames = { default := { explicit := default, varNames := default } }

def Lean.Meta.getMajorTypeIndices (mvarId : Lean.MVarId) (tacticName : Lean.Name) (recursorInfo : Lean.Meta.RecursorInfo) (majorType : Lean.Expr) : Lean.MetaM (Array Lean.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 : Lean.MVarId) (tacticName : Lean.Name) (majorFVarId : Lean.FVarId) (recursorInfo : Lean.Meta.RecursorInfo) (indices : Array Lean.Expr) : Lean.MetaM Lean.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.

Equations

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

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