opaque tactic.customEliminators : Lean.Option Bool

Helper method for creating an user-defined eliminator/recursor application.

structure Lean.Elab.Tactic.ElimApp.Alt : Type

• name : Name

  The short name of the alternative, used in | foo => cases

• info : Meta.ElimAltInfo
• mvarId : MVarId

  The subgoal metavariable for the alternative.

instance Lean.Elab.Tactic.ElimApp.instInhabitedAlt : Inhabited Alt

Equations

• Lean.Elab.Tactic.ElimApp.instInhabitedAlt = { default := Lean.Elab.Tactic.ElimApp.instInhabitedAlt.default }

def Lean.Elab.Tactic.ElimApp.instInhabitedAlt.default : Alt

Equations

• Lean.Elab.Tactic.ElimApp.instInhabitedAlt.default = { name := default, info := default, mvarId := default }

structure Lean.Elab.Tactic.ElimApp.Result : Type

• elimApp : Expr
• elimArgs : Array Expr
• motive : MVarId
• alts : Array Alt
• others : Array MVarId
• complexArgs : Array Expr

def Lean.Elab.Tactic.ElimApp.mkElimApp (elimInfo : Meta.ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result

Construct the an eliminator/recursor application. targets contains the explicit and implicit targets for the eliminator, not yet generalized. For example, the indices of builtin recursors are considered implicit targets. Remark: the method addImplicitTargets may be used to compute the sequence of implicit and explicit targets from the explicit ones.

Equations

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

def Lean.Elab.Tactic.ElimApp.setMotiveArg (mvarId motiveArg : MVarId) (targets : Array FVarId) (complexArgs : Array Expr := #[]) : MetaM Unit

Given a goal ... targets ... |- C[targets, complexArgs] associated with mvarId, where complexArgs are the the complex (i.e. non-target) arguments to the motive in the conclusion of the eliminator, construct motiveArg := fun targets rs => C[targets, rs]

This checks if the type of the complex arguments match what's expected by the motive, and ignores them otherwise. This limits the ability of cases to use unfolding function principles with dependent types, because after generalization of the targets, the types do no longer match. This can likely be improved.

Equations

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

structure Lean.Elab.Tactic.ElimTargetView : Type

View of Lean.Parser.Tactic.elimTarget.

• hIdent? : Option Ident
• term : Syntax

def Lean.Elab.Tactic.mkTargetView (target : Syntax) : TacticM ElimTargetView

Interprets a Lean.Parser.Tactic.elimTarget.

Equations

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

def Lean.Elab.Tactic.elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId))

Elaborates the targets (Lean.Parser.Tactic.elimTarget), generalizing them if requested or if otherwise necessary.

Returns

1. the targets as fvars and
2. an array of identifier/fvarid pairs so that the induction/cases tactic can annotate any user-supplied target hypothesis names using Term.addLocalVarInfo.

Modifies the current goal when generalizing.

Equations

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

def Lean.Elab.Tactic.checkInductionTargets (targets : Array Expr) : MetaM Unit

Equations

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