# Documentation

Lean.Elab.Tactic.Basic

Assign mvarId := sorry

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.
• Declaration name of the executing elaborator, used by mkTacticInfo to persist it in the info tree

elaborator : Lean.Name
• If true, enable "error recovery" in some tactics. For example, cases tactic admits unsolved alternatives when recover == true. The combinator withoutRecover  disables "error recovery" while executing . This is useful for tactics such as first | ... | ....

recover : Bool
Instances For
@[inline]
Equations
@[inline]
Equations
@[always_inline]
Equations
Equations
def Lean.Elab.Tactic.setGoals (mvarIds : ) :
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
def Lean.Elab.Tactic.mkTacticInfo (mctxBefore : Lean.MetavarContext) (goalsBefore : ) (stx : Lean.Syntax) :
Equations
• One or more equations did not get rendered due to their size.
Equations
@[inline]
Equations

Important: we must define evalTactic before we define the instance MonadExcept for TacticM since it backtracks the state including error messages, and this is bad when rethrowing the exception at the catch block in these methods. We marked these places with a (*) in these methods.

Auxiliary datastructure for capturing exceptions at evalTactic.

Instances For
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Tactic.evalTactic.expandEval (stx : Lean.Syntax) (macros : ) (failures : ) :
partial def Lean.Elab.Tactic.evalTactic.eval (stx : Lean.Syntax) (failures : ) :
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.focus {α : Type} (x : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.focusAndDone {α : Type} (tactic : ) :
Equations

Close the main goal using the given tactic. If it fails, log the error and admit

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Elab.Tactic.tryCatch {α : Type} (x : ) (h : ) :
Equations
• = do let b ← Lean.saveState tryCatch x fun ex =>
Equations

Execute x with error recovery disabled

Equations
@[inline]
def Lean.Elab.Tactic.orElse {α : Type} (x : ) (y : ) :
Equations
Equations
• Lean.Elab.Tactic.instOrElseTacticM = { orElse := Lean.Elab.Tactic.orElse }
Equations

Save the current tactic state for a token stx. This method is a no-op if stx has no position information. We use this method to save the tactic state at punctuation such as ;

Equations
• = if then else
@[inline]
def Lean.Elab.Tactic.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (afterStx : Lean.Syntax) (x : ) :

Elaborate x with stx on the macro stack

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

Adapt a syntax transformation to a regular tactic evaluator.

Equations
• = do let stx' ← exp stx
def Lean.Elab.Tactic.appendGoals (mvarIds : ) :

Add the given goals at the end of the current goals collection.

Equations

Discard the first goal and replace it by the given list of goals, keeping the other goals.

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

Return the first goal.

Equations
Equations
• One or more equations did not get rendered due to their size.
• = Lean.Elab.Tactic.throwNoGoalsToBeSolved

Return the main goal metavariable declaration.

Equations

Return the main goal tag.

Equations

Return expected type for the main goal.

Equations

Execute x using the main goal local context and instances

Equations

Evaluate tac at mvarId, and return the list of resulting subgoals.

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.closeMainGoal (val : Lean.Expr) (checkUnassigned : ) :

Close main goal using the given expression. If checkUnassigned == true, then val must not contain unassigned metavariables.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
• One or more equations did not get rendered due to their size.
@[inline]

Get the mvarid of the main goal, run the given tactic, then set the new goals to be the resulting goal list.

Equations
@[inline]
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.tryTactic? {α : Type} (tactic : ) :
Equations
def Lean.Elab.Tactic.tryTactic {α : Type} (tactic : ) :
Equations
def Lean.Elab.Tactic.tagUntaggedGoals (parentTag : Lean.Name) (newSuffix : Lean.Name) (newGoals : ) :

Use parentTag to tag untagged goals at newGoals. If there are multiple new untagged goals, they are named using ._ where idx > 0. If there is only one new untagged goal, then we just use parentTag

Equations
• One or more equations did not get rendered due to their size.
Equations
• = if then else _
def Lean.Elab.Tactic.withCaseRef {m : } {α : Type} [inst : ] [inst : ] (arrow : Lean.Syntax) (body : Lean.Syntax) (x : m α) :
m α

Use position of => \$body for error messages. If there is a line break before body, the message will be displayed on => only, but the "full range" for the info view will still include body`.

Equations