Documentation

Lean.Elab.Tactic.Induction

source
def Lean.Elab.Tactic.isHoleRHS (rhs : Syntax) :
Bool
Equations
source
def Lean.Elab.Tactic.evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) :
TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.

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

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

Instances For
source
instance Lean.Elab.Tactic.ElimApp.instInhabitedAlt :
Inhabited Alt
Equations
source
structure Lean.Elab.Tactic.ElimApp.Context :
Type
source
structure Lean.Elab.Tactic.ElimApp.State :
Type
source
@[reducible, inline]
abbrev Lean.Elab.Tactic.ElimApp.M (α : Type) :
Type
Equations
source
structure Lean.Elab.Tactic.ElimApp.Result :
Type
source
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. 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.
source
partial def Lean.Elab.Tactic.ElimApp.mkElimApp.loop (elimInfo : Meta.ElimInfo) (tag : Name) :
M Unit
source
def Lean.Elab.Tactic.ElimApp.setMotiveArg (mvarId motiveArg : MVarId) (targets : Array FVarId) :
MetaM Unit

Given a goal ... targets ... |- C[targets] associated with mvarId, assign motiveArg := fun targets => C[targets]

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (initialInfo : Info) (numEqs numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) :
TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (numEqs numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) :
TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.ElimApp.evalAlts.goWithIncremental (elimInfo : Meta.ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax)) (numEqs numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) (toTag : Array (Ident × FVarId) := #[]) (tacSnaps : Array (Language.SnapshotBundle TacticParsedSnapshot)) :
TacticM PUnit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.ElimApp.evalAlts.applyAltStx (elimInfo : Meta.ElimInfo) (optPreTac : Syntax) (numEqs numGeneralized : Nat := 0) (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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac (optPreTac : Syntax) (mvarId : MVarId) :
TacticM (List MVarId)

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.getInductiveValFromMajor (induction : Bool) (major : Expr) :
TacticM InductiveVal
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.Elab.Tactic.tactic.customEliminators :
Lean.Option Bool
source
structure Lean.Elab.Tactic.ElimTargetView :
Type

View of Lean.Parser.Tactic.elimTarget.

source
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.
source
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.
source
def Lean.Elab.Tactic.checkInductionTargets (targets : Array Expr) :
MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalInduction :
Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalFunInduction :
Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalCases :
Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalFunCases :
Tactic
Equations
  • One or more equations did not get rendered due to their size.