def Lean.Elab.admitGoal (mvarId : MVarId) (synthetic : Bool := true) : MetaM Unit

Assign mvarId := sorry

def Lean.Elab.goalsToMessageData (goals : List MVarId) : MessageData

def Lean.Elab.Term.reportUnsolvedGoals (goals : List MVarId) : MetaM Unit

structure Lean.Elab.Tactic.Context : Type

• elaborator : Name

  Declaration name of the executing elaborator, used by mkTacticInfo to persist it in the info tree

• recover : Bool

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

@[reducible, inline]

abbrev Lean.Elab.Tactic.TacticM (α : Type) : Type

The tactic monad, which extends the term elaboration monad TermElabM with state that contains the current goals (Lean.Elab.Tactic.State, accessible via MonadStateOf) and local information about the current tactic's name and whether error recovery is enabled (Lean.Elab.Tactic.Context, accessible via MonadReaderOf).

@[reducible, inline]

abbrev Lean.Elab.Tactic.Tactic : Type

A tactic is a function from syntax to an action in the tactic monad.

A given tactic syntax kind may have multiple Tactics associated with it, all of which will be attempted until one succeeds.

@[implicit_reducible, always_inline]

instance Lean.Elab.Tactic.instMonadTacticM : Monad TacticM

@[implicit_reducible]

instance Lean.Elab.Tactic.instInhabitedTacticM {α : Type} : Inhabited (TacticM α)

def Lean.Elab.Tactic.getGoals : TacticM (List MVarId)

Returns the list of goals. Goals may or may not already be assigned.

def Lean.Elab.Tactic.setGoals (mvarIds : List MVarId) : TacticM Unit

def Lean.Elab.Tactic.pruneSolvedGoals : TacticM Unit

def Lean.Elab.Tactic.getUnsolvedGoals : TacticM (List MVarId)

def Lean.Elab.Tactic.run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId)

def Lean.Elab.Tactic.saveState : TacticM SavedState

def Lean.Elab.Tactic.SavedState.restore (b : SavedState) (restoreInfo : Bool := false) : TacticM Unit

@[specialize #[]]

def Lean.Elab.Tactic.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × SavedState)) (tacSnap? : Option (Language.SnapshotBundle TacticParsedSnapshot)) (act : TacticM α) : TacticM (α × SavedState)

Like Meta.withRestoreOrSaveFull for TermElabM, but also takes a tacSnap? that

• when running act, is set as Context.tacSnap?
• otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's value. This extra restore step is necessary because while reusableResult? can be used to replay any effects on State, Context.tacSnap? is not part of it but changed via an IO side effect, so it needs to be replayed separately.

We use an explicit parameter instead of accessing Context.tacSnap? directly because this prevents withRestoreOrSaveFull and withReader from being used in the wrong order.

def Lean.Elab.Tactic.getCurrMacroScope : TacticM MacroScope

def Lean.Elab.Tactic.getMainModule : TacticM Name

opaque Lean.Elab.Tactic.tacticElabAttribute : KeyedDeclsAttribute Tactic

Registers a tactic elaborator for the given syntax node kind.

A tactic elaborator should have type Lean.Elab.Tactic.Tactic (which is Lean.Syntax → Lean.Elab.Tactic.TacticM Unit), i.e. should take syntax of the given syntax node kind as a parameter and alter the tactic state.

The elab_rules and elab commands should usually be preferred over using this attribute directly.

def Lean.Elab.Tactic.mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info

def Lean.Elab.Tactic.mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info)

@[inline]

def Lean.Elab.Tactic.withTacticInfoContext {α : Type} (stx : Syntax) (x : TacticM α) : TacticM α

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.

structure Lean.Elab.Tactic.EvalTacticFailure : Type

Auxiliary datastructure for capturing exceptions at evalTactic.

• exception : Exception
• state : SavedState

partial def Lean.Elab.Tactic.evalTactic (stx : Syntax) : TacticM Unit

def Lean.Elab.Tactic.throwNoGoalsToBeSolved {α : Type} : TacticM α

def Lean.Elab.Tactic.done : TacticM Unit

def Lean.Elab.Tactic.focus {α : Type} (x : TacticM α) : TacticM α

Runs x with only the first unsolved goal as the goal. Fails if there are no goal to be solved.

def Lean.Elab.Tactic.focusAndDone {α : Type} (tactic : TacticM α) : TacticM α

Runs tactic with only the first unsolved goal as the goal, and expects it leave no goals. Fails if there are no goal to be solved.

def Lean.Elab.Tactic.closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit

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

@[implicit_reducible]

instance Lean.Elab.Tactic.instMonadBacktrackSavedStateTacticM : MonadBacktrack SavedState TacticM

@[inline]

def Lean.Elab.Tactic.tryCatch {α : Type} (x : TacticM α) (h : Exception → TacticM α) : TacticM α

Non-backtracking try/catch.

@[inline]

def Lean.Elab.Tactic.tryCatchRestore {α : Type} (x : TacticM α) (h : Exception → TacticM α) : TacticM α

Backtracking try/catch. This is used for the MonadExcept instance for TacticM.

@[implicit_reducible]

instance Lean.Elab.Tactic.instMonadExceptExceptionTacticM : MonadExcept Exception TacticM

def Lean.Elab.Tactic.withoutRecover {α : Type} (x : TacticM α) : TacticM α

Execute x with error recovery disabled

def Lean.Elab.Tactic.withRecover {α : Type} (recover : Bool) (x : TacticM α) : TacticM α

Execute x with error recovery disabled

Message log utilities

def Lean.Elab.Tactic.withSuppressedMessages {α : Type} (action : TacticM α) : TacticM α

Execute an action while suppressing any new messages it generates. Restores the original message log after the action completes. Useful for trying tactics without polluting the message log with errors from failed attempts.

def Lean.Elab.Tactic.withCapturedMessages {α : Type} (action : TacticM α) : TacticM (α × List Message)

Execute an action and return any new messages it generates. Restores the original message log afterward. Useful for inspecting messages produced by a tactic without committing them.

def Lean.Elab.Tactic.hasErrorMessages (msgs : List Message) : Bool

Check if any messages in the list are errors.

def Lean.Elab.Tactic.throwOrLogErrorAt (ref : Syntax) (msg : MessageData) : TacticM Unit

Like throwErrorAt, but, if recovery is enabled, logs the error instead.

def Lean.Elab.Tactic.throwOrLogError (msg : MessageData) : TacticM Unit

Like throwError, but, if recovery is enabled, logs the error instead.

@[inline]

def Lean.Elab.Tactic.orElse {α : Type} (x : TacticM α) (y : Unit → TacticM α) : TacticM α

@[implicit_reducible]

instance Lean.Elab.Tactic.instOrElseTacticM {α : Type} : OrElse (TacticM α)

@[implicit_reducible]

instance Lean.Elab.Tactic.instAlternativeTacticM : Alternative TacticM

def Lean.Elab.Tactic.saveTacticInfoForToken (stx : Syntax) : TacticM Unit

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 ;

@[inline]

def Lean.Elab.Tactic.withMacroExpansion {α : Type} (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α

Elaborate x with stx on the macro stack

def Lean.Elab.Tactic.adaptExpander (exp : Syntax → TacticM Syntax) : Tactic

Adapt a syntax transformation to a regular tactic evaluator.

def Lean.Elab.Tactic.pushGoal (mvarId : MVarId) : TacticM Unit

Add the given goal to the front of the current list of goals.

def Lean.Elab.Tactic.pushGoals (mvarIds : List MVarId) : TacticM Unit

Add the given goals to the front of the current list of goals.

def Lean.Elab.Tactic.appendGoals (mvarIds : List MVarId) : TacticM Unit

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

def Lean.Elab.Tactic.replaceMainGoal (mvarIds : List MVarId) : TacticM Unit

Discard the first goal and replace it by the given list of goals, keeping the other goals. This is used in conjunction with getMainGoal.

Contract: between getMainGoal and replaceMainGoal, nothing manipulates the goal list.

See also Lean.Elab.Tactic.popMainGoal and Lean.Elab.Tactic.pushGoal/Lean.Elab.Tactic.pushGoal for another interface.

def Lean.Elab.Tactic.getMainGoal : TacticM MVarId

Return the first goal.

def Lean.Elab.Tactic.popMainGoal : TacticM MVarId

Return the first goal, and remove it from the goal list.

See also: Lean.Elab.Tactic.pushGoal and Lean.Elab.Tactic.pushGoals.

def Lean.Elab.Tactic.getMainDecl : TacticM MetavarDecl

Return the main goal metavariable declaration.

def Lean.Elab.Tactic.getMainTag : TacticM Name

Return the main goal tag.

def Lean.Elab.Tactic.getMainTarget : TacticM Expr

Return expected type for the main goal.

def Lean.Elab.Tactic.withMainContext {α : Type} (x : TacticM α) : TacticM α

Execute x using the main goal local context and instances

def Lean.Elab.Tactic.evalTacticAt (tac : Syntax) (mvarId : MVarId) : TacticM (List MVarId)

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

def Lean.Elab.Tactic.evalTacticAtRaw (tac : Syntax) (mvarId : MVarId) : TacticM (List MVarId)

Like evalTacticAt, but without restoring the goal list or pruning solved goals. Useful when these tasks are already being done in an outer loop.

def Lean.Elab.Tactic.ensureHasNoMVars (e : Expr) : TacticM Unit

def Lean.Elab.Tactic.closeMainGoal (tacName : Name) (val : Expr) (checkUnassigned : Bool := true) : TacticM Unit

Closes main goal using the given expression. If checkUnassigned == true, then val must not contain unassigned metavariables. Returns true if val was successfully used to close the goal.

@[inline]

def Lean.Elab.Tactic.liftMetaMAtMain {α : Type} (x : MVarId → MetaM α) : TacticM α

@[inline]

def Lean.Elab.Tactic.liftMetaTacticAux {α : Type} (tac : MVarId → MetaM (α × List MVarId)) : TacticM α

@[inline]

def Lean.Elab.Tactic.liftMetaTactic (tactic : MVarId → MetaM (List MVarId)) : TacticM Unit

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

@[inline]

def Lean.Elab.Tactic.liftMetaTactic1 (tactic : MVarId → MetaM (Option MVarId)) : TacticM Unit

@[inline]

def Lean.Elab.Tactic.liftMetaFinishingTactic (tac : MVarId → MetaM Unit) : TacticM Unit

Analogue of liftMetaTactic for tactics that do not return any goals.

def Lean.Elab.Tactic.tryTactic? {α : Type} (tactic : TacticM α) : TacticM (Option α)

def Lean.Elab.Tactic.tryTactic {α : Type} (tactic : TacticM α) : TacticM Bool

def Lean.Elab.Tactic.tagUntaggedGoals (parentTag newSuffix : Name) (newGoals : List MVarId) : TacticM Unit

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

def Lean.Elab.Tactic.getNameOfIdent' (id : Syntax) : Name

def Lean.Elab.Tactic.withCaseRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (arrow body : 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.