evalGRewriteSeq

Mathlib.Tactic.GRewrite.Elab

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

Lean4

@[tactic grewriteSeq, inherit_doc grewriteSeq]
def evalGRewriteSeq : Tactic := fun stx => do
  let cfg ← elabGRewriteConfig stx[1]
  let loc := expandOptLocation stx[3]
  withRWRulesSeq stx[0] stx[2] fun symm term => do
      withLocation loc (grewriteLocalDecl term symm · cfg) (grewriteTarget term symm cfg)
          (throwTacticEx `grewrite · "did not find instance of the pattern in the current goal")

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

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

Разделы

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

Аффилиация

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