tacticSyntax

Mathlib.Tactic.Widget.LibraryRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LibraryRewrite.tacticSyntax

Lean4

/-- Return the rewrite tactic that performs the rewrite. -/
def tacticSyntax (rw : Rewrite) (occ : Option Nat) (loc : Option Name) : MetaM (TSyntax `tactic) :=
  withoutModifyingMCtx do
    -- we want the new metavariables to be printed as `?_` in the tactic syntax

    for (mvarId, _) in rw.extraGoals do
      mvarId.setTag .anonymous
    let proof ← withOptions (pp.mvars.anonymous.set · false) (PrettyPrinter.delab rw.proof)
    mkRewrite occ rw.symm proof loc

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

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

Разделы

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

Аффилиация

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