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

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.

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

• name : Lake.Name

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

• declName? : Option Lake.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.

• mvarId : Lean.MVarId

  The subgoal metavariable for the alternative.

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 } }

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

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

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

@[inline, reducible]

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)

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

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

def Lean.Elab.Tactic.ElimApp.mkElimApp (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (tag : Lake.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.

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

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.

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

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

def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Lean.Meta.ElimInfo) (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (optPreTac : Lean.Syntax) (altsSyntax : Array Lean.Syntax) (initialInfo : Lean.Elab.Info) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.ElimApp.evalAlts.go (elimInfo : Lean.Meta.ElimInfo) (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (optPreTac : Lean.Syntax) (altsSyntax : Array Lean.Syntax) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) : Lean.Elab.Tactic.TacticM Unit

Equations

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

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

Equations

• Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac optPreTac mvarId = if Lean.Syntax.isNone optPreTac = true then pure [mvarId] else Lean.Elab.Tactic.evalTacticAt optPreTac[0] mvarId

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

Equations

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

def Lean.Elab.Tactic.evalInduction : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

def Lean.Elab.Tactic.elabCasesTargets (targets : Array Lean.Syntax) : Lean.Elab.Tactic.TacticM (Array Lean.Expr)

Equations

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

def Lean.Elab.Tactic.evalCases : Lean.Elab.Tactic.Tactic

Equations

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