Lean.Elab.Tactic.Induction

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

Equations

Lean.Elab.Tactic.isHoleRHS rhs = (Lean.Syntax.isOfKind rhs `Lean.Parser.Term.syntheticHole || Lean.Syntax.isOfKind rhs `Lean.Parser.Term.hole)

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

Lean.Elab.Tactic.TacticM (Array Lean.MVarId)

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

The short name of the alternative, used in | foo => cases
name : Lean.Name
A declaration corresponding to the inductive constructor. (For custom recursors, the alternatives correspond to parameter names in the recursor, so we may not have a declaration to point to.) This is used for go-to-definition on the alternative name.
declName? : Option Lean.Name
The subgoal metavariable for the alternative.
mvarId : Lean.MVarId

Instances For

source

instance Lean.Elab.Tactic.ElimApp.instInhabitedAlt :

Inhabited Lean.Elab.Tactic.ElimApp.Alt

Equations

Lean.Elab.Tactic.ElimApp.instInhabitedAlt = { default := { name := default, declName? := default, mvarId := default } }

source

structure Lean.Elab.Tactic.ElimApp.Context :

Type

elimInfo : Lean.Meta.ElimInfo
targets : Array Lean.Expr

Instances For

source

structure Lean.Elab.Tactic.ElimApp.State :

Type

argPos : Nat
targetPos : Nat
f : Lean.Expr
fType : Lean.Expr
alts : Array Lean.Elab.Tactic.ElimApp.Alt
insts : Array Lean.MVarId

Instances For

source

@[inline]

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

Type

Equations

Lean.Elab.Tactic.ElimApp.M = ReaderT Lean.Elab.Tactic.ElimApp.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.ElimApp.State Lean.Elab.TermElabM)

source

structure Lean.Elab.Tactic.ElimApp.Result :

Type

elimApp : Lean.Expr
alts : Array Lean.Elab.Tactic.ElimApp.Alt
others : Array Lean.MVarId

Instances For

source

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

Lean.Elab.TermElabM Lean.Elab.Tactic.ElimApp.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 : Lean.Meta.ElimInfo) (tag : Lean.Name) :

Lean.Elab.Tactic.ElimApp.M Unit

source

def Lean.Elab.Tactic.ElimApp.setMotiveArg (mvarId : Lean.MVarId) (motiveArg : Lean.MVarId) (targets : Array Lean.FVarId) :

Lean.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.reorderAlts (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (altsSyntax : Array Lean.Syntax) :

Array Lean.Elab.Tactic.ElimApp.Alt

If altsSyntax is not empty we reorder alts using the order the alternatives have been provided in altsSyntax. Motivations:

1- It improves the effectiveness of the checkpoint and save tactics. Consider the following example:

example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
  cases h₁ with
  | inr h =>
    sleep 5000 -- sleeps for 5 seconds
    save
    have : y = 0 := h₃ h
    -- We can confortably work here
  | inl h => stop ...

If we do reorder, the inl alternative will be executed first. Moreover, as we type in the inr alternative, type errors will "swallow" the inl alternative and affect the tactic state at save making it ineffective.

2- The errors are produced in the same order the appear in the code above. This is not super important when using IDEs.

Equations