Documentation

Lean.Meta.Tactic.Induction

structure Lean.Meta.InductionSubgoal:

Type

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.induction (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (recursorName : Lean.Name) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :

Lean.MetaM (Array Lean.Meta.InductionSubgoal)

Equations

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