structure Lean.Meta.InductionSubgoal : Type

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

Instances For

• Lean.Meta.instInhabitedInductionSubgoal

instance Lean.Meta.instInhabitedInductionSubgoal : Inhabited InductionSubgoal

Equations

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

structure Lean.Meta.AltVarNames : Type

• explicit : Bool
• varNames : List Name

Instances For

• Lean.Meta.instInhabitedAltVarNames

instance Lean.Meta.instInhabitedAltVarNames : Inhabited AltVarNames

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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