focusAndDoneWithScope

Mathlib.Lean.Elab.Tactic.Basic

URI: https://scilib.ai/kg/mathlib#Lean.Elab.Tactic.focusAndDoneWithScope

Lean4

/-- Like `focusAndDone` but takes a scope (e.g. tactic name) as an argument to
produce more detailed error messages.
-/
def focusAndDoneWithScope {α : Type} (scope : MessageData) (tactic : TacticM α) : TacticM α :=
  focus do
    let a ←
      try
        tactic
      catch e =>
        if isAbortTacticException e then
          throw e
        else
          throwError "{scope} failed.\n{← nestedExceptionToMessageData e}"
    doneWithScope scope
    pure a

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru