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. 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) :

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