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

Assign `mvarId := sorry`

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

source
@[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`).

Equations

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

Instances For

source
@[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 `Tactic`s associated with it, all of which will be attempted until one succeeds.

Equations

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

Instances For

source
@[always_inline]
instance Lean.Elab.Tactic.instMonadTacticM :
Monad TacticM
Equations

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

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

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

source
def Lean.Elab.Tactic.getGoals :
TacticM (List 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

Instances For

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

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

Instances For

source
def Lean.Elab.Tactic.pruneSolvedGoals :
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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Elab.Tactic.saveState :
TacticM 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 }

Instances For

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

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

Instances For

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

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

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

Instances For

source
def Lean.Elab.Tactic.mkInitialTacticInfo (stx : Syntax) :
TacticM (TacticM 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)

Instances For

source
@[inline]
def Lean.Elab.Tactic.withTacticInfoContext {α : Type} (stx : Syntax) (x : TacticM α) :
TacticM α
Equations

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

Instances For

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.

source
structure Lean.Elab.Tactic.EvalTacticFailure :
Type

Auxiliary datastructure for capturing exceptions at `evalTactic`.

- exception : Exception
- state : SavedState

Instances For

source
partial def Lean.Elab.Tactic.evalTactic (stx : Syntax) :
TacticM Unit
source
def Lean.Elab.Tactic.throwNoGoalsToBeSolved {α : Type} :
TacticM α
Equations

- Lean.Elab.Tactic.throwNoGoalsToBeSolved = Lean.throwError (Lean.toMessageData "No goals to be solved")

Instances For

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

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

source
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`

Equations

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

Instances For

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

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

source
@[inline]
def Lean.Elab.Tactic.tryCatch {α : Type} (x : TacticM α) (h : Exception → TacticM α) :
TacticM α

Non-backtracking `try`/`catch`.

Equations

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

Instances For

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

Equations

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

Instances For

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

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

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

Instances For

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

Execute `x` with error recovery disabled

Equations

- Lean.Elab.Tactic.withRecover recover x = withReader (fun (ctx : Lean.Elab.Tactic.Context) => { elaborator := ctx.elaborator, recover := recover }) x

Instances For

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

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

Equations

- Lean.Elab.Tactic.throwOrLogErrorAt ref msg = do let __do_lift ← read if __do_lift.recover = true then Lean.logErrorAt ref msg else Lean.throwErrorAt ref msg

Instances For

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

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

Equations

- Lean.Elab.Tactic.throwOrLogError msg = do let __do_lift ← Lean.getRef Lean.Elab.Tactic.throwOrLogErrorAt __do_lift msg

Instances For

source
@[inline]
def Lean.Elab.Tactic.orElse {α : Type} (x : TacticM α) (y : Unit → TacticM α) :
TacticM α
Equations

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

Instances For

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

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

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

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

source
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 `;`

Equations

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

Instances For

source
@[inline]
def Lean.Elab.Tactic.withMacroExpansion {α : Type} (beforeStx afterStx : Syntax) (x : TacticM α) :
TacticM α

Elaborate `x` with `stx` on the macro stack

Equations

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

Instances For

source
def Lean.Elab.Tactic.adaptExpander (exp : Syntax → TacticM Syntax) :
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')

Instances For

source
def Lean.Elab.Tactic.pushGoal (mvarId : MVarId) :
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 }

Instances For

source
def Lean.Elab.Tactic.pushGoals (mvarIds : List MVarId) :
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 }

Instances For

source
def Lean.Elab.Tactic.appendGoals (mvarIds : List MVarId) :
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 }

Instances For

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

Equations

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

Instances For

source
def Lean.Elab.Tactic.getMainGoal :
TacticM 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

Instances For

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

Equations

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

Instances For

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

Return the main goal metavariable declaration.

Equations

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

Instances For

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

Return the main goal tag.

Equations

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

Instances For

source
def Lean.Elab.Tactic.getMainTarget :
TacticM 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

Instances For

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

Instances For

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

Instances For

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

Equations

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

Instances For

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

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

Instances For

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

Equations

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

Instances For

source
@[inline]
def Lean.Elab.Tactic.liftMetaMAtMain {α : Type} (x : MVarId → MetaM α) :
TacticM α
Equations

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

Instances For

source
@[inline]
def Lean.Elab.Tactic.liftMetaTacticAux {α : Type} (tac : MVarId → MetaM (α × List MVarId)) :
TacticM α
Equations

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

Instances For

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

Equations

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

Instances For

source
@[inline]
def Lean.Elab.Tactic.liftMetaTactic1 (tactic : MVarId → MetaM (Option MVarId)) :
TacticM Unit
Equations

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

Instances For

source
@[inline]
def Lean.Elab.Tactic.liftMetaFinishingTactic (tac : MVarId → MetaM Unit) :
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 []

Instances For

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

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

Instances For

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

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

Instances For

source
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`

Equations

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

Instances For

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

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

Instances For

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

Equations

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

Instances For