Documentation

Lean.Elab.Tactic.Induction

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

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

  • name : Name

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

  • mvarId : MVarId

    The subgoal metavariable for the alternative.

Instances For

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 := #[]) :

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.
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) := #[]) :
Equations
  • One or more equations did not get rendered due to their size.
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) := #[]) :
Equations
  • One or more equations did not get rendered due to their size.
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)) :
Equations
  • One or more equations did not get rendered due to their size.
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) :

Applies syntactic alternative to alternative goal.

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

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

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

Interprets a Lean.Parser.Tactic.elimTarget.

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

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.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

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.
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.evalCasesCore (stx : Syntax) (elimInfo : Meta.ElimInfo) (targets : Array Expr) (toTag : Array (Ident × FVarId) := #[]) :

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.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.