def Lean.Elab.Tactic.isHoleRHS (rhs : Syntax) : Bool

def Lean.Elab.Tactic.evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : TacticM Unit

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

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

• elimInfo : Meta.ElimInfo
• targets : Array Expr

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

• argPos : Nat
• targetPos : Nat
• motive : Option MVarId
• f : Expr
• fType : Expr
• alts : Array Alt
• insts : Array MVarId

@[reducible, inline]

abbrev Lean.Elab.Tactic.ElimApp.M (α : Type) : Type

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.

partial def Lean.Elab.Tactic.ElimApp.mkElimApp.loop (elimInfo : Meta.ElimInfo) (tag : Name) : M Unit

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.

def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (initialInfo : Info) (tacStx : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit

def Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (tacStx : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit

def Lean.Elab.Tactic.ElimApp.evalAlts.goWithIncremental (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (tacStx : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) (tacSnaps : Array (Language.SnapshotBundle TacticParsedSnapshot)) : TacticM PUnit

def Lean.Elab.Tactic.ElimApp.evalAlts.applyAltStx (elimInfo : Meta.ElimInfo) (optPreTac : Syntax) (numEqs : Nat := 0) (generalized toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) (tacSnaps : Array (Language.SnapshotBundle TacticParsedSnapshot)) (altStxs : Array Syntax) (altStxIdx : Nat) (altStx : Syntax) (alt : Alt) : TacticM PUnit

Applies syntactic alternative to alternative goal.

def Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac (optPreTac : Syntax) (mvarId : MVarId) : TacticM (List MVarId)

Applies induction .. with $preTac | .., if any, to an alternative goal.

def Lean.Elab.Tactic.getInductiveValFromMajor (induction : Bool) (major : Expr) : TacticM InductiveVal

opaque Lean.Elab.Tactic.tactic.customEliminators : Lean.Option Bool

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.

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.

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

def Lean.Elab.Tactic.evalInduction : Tactic

opaque Lean.Elab.Tactic.tactic.fun_induction.unfolding : Lean.Option Bool

def Lean.Elab.Tactic.elabFunTargetCall (cases : Bool) (stx : Syntax) : TacticM Expr

Elaborates the foo args of fun_induction or fun_cases, inferring the args if omitted from the goal

def Lean.Elab.Tactic.evalFunInduction : Tactic

def Lean.Elab.Tactic.evalCasesCore (stx : Syntax) (elimInfo : Meta.ElimInfo) (targets : Array Expr) (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit

The code path shared between cases and fun_cases; when we already have an elimInfo and the targets contains the implicit targets

def Lean.Elab.Tactic.evalCases : Tactic

def Lean.Elab.Tactic.evalFunCases : Tactic