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

Assign mvarId := sorry

Equations

• Lean.Elab.admitGoal mvarId = mvarId.withContext do let mvarType ← Lean.Meta.inferType (Lean.mkMVar mvarId) let __do_lift ← Lean.Meta.mkSorry mvarType true mvarId.assign __do_lift

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

Equations

• Lean.Elab.goalsToMessageData goals = Lean.MessageData.joinSep (List.map Lean.MessageData.ofGoal goals) (Lean.toMessageData "\n\n")

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

Equations

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

structure Lean.Elab.Tactic.Context : Type

• elaborator : Lean.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

Equations

• Lean.Elab.Tactic.TacticM = ReaderT Lean.Elab.Tactic.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.State Lean.Elab.TermElabM)

@[reducible, inline]

abbrev Lean.Elab.Tactic.Tactic : Type

Equations

• Lean.Elab.Tactic.Tactic = (Lean.Syntax → Lean.Elab.Tactic.TacticM Unit)

@[always_inline]

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

Equations

• Lean.Elab.Tactic.instMonadTacticM = Monad.mk

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

Equations

• Lean.Elab.Tactic.instInhabitedTacticM = { default := fun (x : Lean.Elab.Tactic.Context) (x : ST.Ref IO.RealWorld Lean.Elab.Tactic.State) => default }

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

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

Equations

• Lean.Elab.Tactic.getGoals = do let __do_lift ← get pure __do_lift.goals

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

Equations

• Lean.Elab.Tactic.setGoals mvarIds = modify fun (x : Lean.Elab.Tactic.State) => { goals := mvarIds }

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

Equations

• Lean.Elab.Tactic.pruneSolvedGoals = do let gs ← Lean.Elab.Tactic.getGoals let gs ← List.filterM (fun (g : Lean.MVarId) => not <$> g.isAssigned) gs Lean.Elab.Tactic.setGoals gs

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

Equations

• Lean.Elab.Tactic.getUnsolvedGoals = do Lean.Elab.Tactic.pruneSolvedGoals Lean.Elab.Tactic.getGoals

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

Equations

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

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

Equations

• Lean.Elab.Tactic.saveState = do let __do_lift ← liftM Lean.Elab.Term.saveState let __do_lift_1 ← get pure { term := __do_lift, tactic := __do_lift_1 }

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

Equations

• b.restore restoreInfo = do liftM (b.term.restore restoreInfo) set b.tactic

@[specialize #[]]

def Lean.Elab.Tactic.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × Lean.Elab.Tactic.SavedState)) (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)) (act : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM (α × Lean.Elab.Tactic.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.

Equations

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

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

Equations

• Lean.Elab.Tactic.getCurrMacroScope = do let __do_lift ← readThe Lean.Core.Context pure __do_lift.currMacroScope

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

Equations

• Lean.Elab.Tactic.getMainModule = do let __do_lift ← Lean.getEnv pure __do_lift.mainModule

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

Equations

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

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

Equations

• Lean.Elab.Tactic.mkInitialTacticInfo stx = do let mctxBefore ← Lean.getMCtx let goalsBefore ← Lean.Elab.Tactic.getUnsolvedGoals pure (Lean.Elab.Tactic.mkTacticInfo mctxBefore goalsBefore stx)

@[inline]

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

Equations

• Lean.Elab.Tactic.withTacticInfoContext stx x = do let __do_lift ← Lean.Elab.Tactic.mkInitialTacticInfo stx Lean.Elab.withInfoContext x __do_lift

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 : Lean.Exception
• state : Lean.Elab.Tactic.SavedState

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

Equations

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

@[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

Equations

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

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 α

Equations

• Lean.Elab.Tactic.throwNoGoalsToBeSolved = Lean.throwError (Lean.toMessageData "no goals to be solved")

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.focusAndDone tactic = Lean.Elab.Tactic.focus do let a ← tactic Lean.Elab.Tactic.done pure a

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

Equations

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

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

Equations

• Lean.Elab.Tactic.instMonadBacktrackSavedStateTacticM = { saveState := Lean.Elab.Tactic.saveState, restoreState := fun (b : Lean.Elab.Tactic.SavedState) => b.restore }

@[inline]

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

Non-backtracking try/catch.

Equations

• Lean.Elab.Tactic.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => h ex

@[inline]

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

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

Equations

• Lean.Elab.Tactic.tryCatchRestore x h = do let b ← Lean.saveState tryCatch x fun (ex : Lean.Exception) => do b.restore h ex

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

Equations

• Lean.Elab.Tactic.instMonadExceptExceptionTacticM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Elab.Tactic.tryCatchRestore }

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

Execute x with error recovery disabled

Equations

• Lean.Elab.Tactic.withoutRecover x = withReader (fun (ctx : Lean.Elab.Tactic.Context) => { elaborator := ctx.elaborator, recover := false }) x

@[inline]

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

Equations

• Lean.Elab.Tactic.orElse x y = tryCatch (Lean.Elab.Tactic.withoutRecover x) fun (x : Lean.Exception) => y ()

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

Equations

• Lean.Elab.Tactic.instOrElseTacticM = { orElse := Lean.Elab.Tactic.orElse }

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

Equations

• Lean.Elab.Tactic.instAlternativeTacticM = Alternative.mk (fun {x : Type} => Lean.throwError (Lean.toMessageData "failed")) fun {α : Type} => Lean.Elab.Tactic.orElse

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 ;

Equations

• Lean.Elab.Tactic.saveTacticInfoForToken stx = if stx.getPos?.isNone = true then pure PUnit.unit else Lean.Elab.Tactic.withTacticInfoContext stx (pure ())

@[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

Equations

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

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.

Equations

• Lean.Elab.Tactic.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Tactic.withMacroExpansion stx stx' (Lean.Elab.Tactic.evalTactic stx')

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

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

Equations

• Lean.Elab.Tactic.pushGoal mvarId = modify fun (s : Lean.Elab.Tactic.State) => { goals := mvarId :: s.goals }

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

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

Equations

• Lean.Elab.Tactic.pushGoals mvarIds = modify fun (s : Lean.Elab.Tactic.State) => { goals := mvarIds ++ s.goals }

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

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

Equations

• Lean.Elab.Tactic.appendGoals mvarIds = modify fun (s : Lean.Elab.Tactic.State) => { goals := s.goals ++ mvarIds }

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

Equations

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

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

Return the first goal.

Equations

• Lean.Elab.Tactic.getMainGoal = do let __do_lift ← Lean.Elab.Tactic.getGoals Lean.Elab.Tactic.getMainGoal.loop __do_lift

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.popMainGoal : Lean.Elab.Tactic.TacticM Lean.MVarId

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

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

Equations

• Lean.Elab.Tactic.popMainGoal = do let mvarId ← Lean.Elab.Tactic.getMainGoal Lean.Elab.Tactic.replaceMainGoal [] pure mvarId

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

Return the main goal metavariable declaration.

Equations

• Lean.Elab.Tactic.getMainDecl = do let __do_lift ← Lean.Elab.Tactic.getMainGoal liftM __do_lift.getDecl

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

Return the main goal tag.

Equations

• Lean.Elab.Tactic.getMainTag = do let __do_lift ← Lean.Elab.Tactic.getMainDecl pure __do_lift.userName

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

Return expected type for the main goal.

Equations

• Lean.Elab.Tactic.getMainTarget = do let __do_lift ← Lean.Elab.Tactic.getMainDecl Lean.instantiateMVars __do_lift.type

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

Equations

• Lean.Elab.Tactic.withMainContext x = do let __do_lift ← Lean.Elab.Tactic.getMainGoal __do_lift.withContext x

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.

Equations

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

def Lean.Elab.Tactic.evalTacticAtRaw (tac : Lean.Syntax) (mvarId : Lean.MVarId) : Lean.Elab.Tactic.TacticM (List Lean.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.

Equations

• Lean.Elab.Tactic.evalTacticAtRaw tac mvarId = do Lean.Elab.Tactic.setGoals [mvarId] Lean.Elab.Tactic.evalTactic tac Lean.Elab.Tactic.getGoals

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

Equations

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

def Lean.Elab.Tactic.closeMainGoal (tacName : Lean.Name) (val : Lean.Expr) (checkUnassigned : optParam Bool true) : Lean.Elab.Tactic.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.

Equations

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

@[inline]

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

Equations

• Lean.Elab.Tactic.liftMetaMAtMain x = Lean.Elab.Tactic.withMainContext do let __do_lift ← Lean.Elab.Tactic.getMainGoal liftM (x __do_lift)

@[inline]

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

Equations

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

@[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.

Equations

• Lean.Elab.Tactic.liftMetaTactic tactic = Lean.Elab.Tactic.liftMetaTacticAux fun (mvarId : Lean.MVarId) => do let gs ← tactic mvarId pure ((), gs)

@[inline]

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

Equations

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

@[inline]

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

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

Equations

• Lean.Elab.Tactic.liftMetaFinishingTactic tac = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => do tac g pure []

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

Equations

• Lean.Elab.Tactic.tryTactic? tactic = tryCatch (do let __do_lift ← tactic pure (some __do_lift)) fun (x : Lean.Exception) => pure none

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

Equations

• Lean.Elab.Tactic.tryTactic tactic = tryCatch (do discard tactic pure true) fun (x : Lean.Exception) => pure false

def Lean.Elab.Tactic.tagUntaggedGoals (parentTag : Lean.Name) (newSuffix : Lean.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 <parentTag>.<newSuffix>_<idx> 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.

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

Equations

• Lean.Elab.Tactic.getNameOfIdent' id = if id.isIdent = true then id.getId else `_

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.

Equations

• Lean.Elab.Tactic.withCaseRef arrow body x = Lean.withRef (Lean.mkNullNode #[arrow, body]) x