evalDepRewriteSeq

Mathlib.Tactic.DepRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.DepRewrite.Conv.evalDepRewriteSeq

Lean4

@[tactic depRewrite, inherit_doc depRewriteSeq]
def evalDepRewriteSeq : Tactic := fun stx => do
  let cfg ← elabDepRewriteConfig stx[1]
  let loc := expandOptLocation stx[3]
  withRWRulesSeq stx[0] stx[2] fun symm term => do
      withLocation loc (DepRewrite.depRewriteLocalDecl term symm · cfg) (depRewriteTarget term symm cfg)
          (throwTacticEx `depRewrite · "did not find instance of the pattern in the current goal")

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

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

Разделы

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

Аффилиация

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