source
structure Lean.Meta.InductionSubgoal :
Type

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

Instances For

source
instance Lean.Meta.instInhabitedInductionSubgoal :
Inhabited InductionSubgoal
Equations

- Lean.Meta.instInhabitedInductionSubgoal = { default := Lean.Meta.instInhabitedInductionSubgoal.default }

source
def Lean.Meta.instInhabitedInductionSubgoal.default :
InductionSubgoal
Equations

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

Instances For

source
structure Lean.Meta.AltVarNames :
Type

- explicit : Bool
- varNames : List Name

Instances For

source
instance Lean.Meta.instInhabitedAltVarNames :
Inhabited AltVarNames
Equations

- Lean.Meta.instInhabitedAltVarNames = { default := Lean.Meta.instInhabitedAltVarNames.default }

source
def Lean.Meta.instInhabitedAltVarNames.default :
AltVarNames
Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For