structure Lean.Meta.InductionSubgoal : Type

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

Instances For

• Lean.Meta.instInhabitedInductionSubgoal

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 Lake.Name

Instances For

• Lean.Meta.instInhabitedAltVarNames

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

Equations

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

def Lean.MVarId.induction (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (recursorName : Lake.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.

@[deprecated Lean.MVarId.induction]

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

Equations

• Lean.Meta.induction mvarId majorFVarId recursorName givenNames = Lean.MVarId.induction mvarId majorFVarId recursorName givenNames