def Lean.Elab.admitGoal (mvarId : Lean.MVarId) : Lean.MetaM Unit

Assign mvarId := sorry

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

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

structure Lean.Elab.Tactic.Context : Type

• elaborator : Lake.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 disables "error recovery" while executing . This is useful for tactics such as first | ... | ....

structure Lean.Elab.Tactic.SavedState : Type

• term : Lean.Elab.Term.SavedState
• tactic : Lean.Elab.Tactic.State

@[inline, reducible]

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

@[inline, reducible]

abbrev Lean.Elab.Tactic.Tactic : Type

@[always_inline]

instance Lean.Elab.Tactic.instMonadTacticM : Monad Lean.Elab.Tactic.TacticM

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

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

def Lean.Elab.Tactic.pruneSolvedGoals : Lean.Elab.Tactic.TacticM Unit

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

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

def Lean.Elab.Tactic.saveState : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.SavedState

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

def Lean.Elab.Tactic.getCurrMacroScope : Lean.Elab.Tactic.TacticM Lean.MacroScope

def Lean.Elab.Tactic.getMainModule : Lean.Elab.Tactic.TacticM Lake.Name

unsafe def Lean.Elab.Tactic.mkTacticAttribute : IO (Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Tactic)

opaque Lean.Elab.Tactic.tacticElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Tactic

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

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

@[inline]

def Lean.Elab.Tactic.withTacticInfoContext {α : Type} (stx : Lean.Syntax) (x : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.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

• exception : Lean.Exception
• state : Lean.Elab.Tactic.SavedState

Auxiliary datastructure for capturing exceptions at evalTactic.

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

def Lean.Elab.Tactic.evalTactic.throwExs (stx : Lean.Syntax) (failures : Array Lean.Elab.Tactic.EvalTacticFailure) : Lean.Elab.Tactic.TacticM Unit

@[inline]

def Lean.Elab.Tactic.evalTactic.handleEx (s : Lean.Elab.Tactic.SavedState) (failures : Array Lean.Elab.Tactic.EvalTacticFailure) (ex : Lean.Exception) (k : Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

partial def Lean.Elab.Tactic.evalTactic.expandEval (stx : Lean.Syntax) (s : Lean.Elab.Tactic.SavedState) (macros : List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Macro)) (evalFns : List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Tactic)) (failures : Array Lean.Elab.Tactic.EvalTacticFailure) : Lean.Elab.Tactic.TacticM Unit

partial def Lean.Elab.Tactic.evalTactic.eval (stx : Lean.Syntax) (s : Lean.Elab.Tactic.SavedState) (evalFns : List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Tactic)) (failures : Array Lean.Elab.Tactic.EvalTacticFailure) : Lean.Elab.Tactic.TacticM Unit

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

def Lean.Elab.Tactic.done : Lean.Elab.Tactic.TacticM Unit

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

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

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

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

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

@[inline]

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

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

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

Execute x with error recovery disabled

@[inline]

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

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

instance Lean.Elab.Tactic.instAlternativeTacticM : Alternative Lean.Elab.Tactic.TacticM

def Lean.Elab.Tactic.saveTacticInfoForToken (stx : Lean.Syntax) : Lean.Elab.Tactic.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 : Lean.Syntax) (afterStx : Lean.Syntax) (x : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

Elaborate x with stx on the macro stack

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

Adapt a syntax transformation to a regular tactic evaluator.

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

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

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

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

def Lean.Elab.Tactic.getMainGoal : Lean.Elab.Tactic.TacticM Lean.MVarId

Return the first goal.

def Lean.Elab.Tactic.getMainGoal.loop : List Lean.MVarId → Lean.Elab.Tactic.TacticM Lean.MVarId

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.getMainGoal.loop [] = Lean.Elab.Tactic.throwNoGoalsToBeSolved

def Lean.Elab.Tactic.getMainDecl : Lean.Elab.Tactic.TacticM Lean.MetavarDecl

Return the main goal metavariable declaration.

def Lean.Elab.Tactic.getMainTag : Lean.Elab.Tactic.TacticM Lake.Name

Return the main goal tag.

def Lean.Elab.Tactic.getMainTarget : Lean.Elab.Tactic.TacticM Lean.Expr

Return expected type for the main goal.

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

Execute x using the main goal local context and instances

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

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

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

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

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

@[inline]

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

@[inline]

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

@[inline]

def Lean.Elab.Tactic.liftMetaTactic (tactic : Lean.MVarId → Lean.MetaM (List Lean.MVarId)) : Lean.Elab.Tactic.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 : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)) : Lean.Elab.Tactic.TacticM Unit

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

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

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

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

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

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