M

Mathlib.Tactic.DepRewrite

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

Lean4

/-- Monad for computing `dabstract`.

The `Nat` state tracks which occurrence of the pattern we are about to see, 1-indexed
(so the initial value is `1`).

The cache stores results of `visit` together with
- the `Nat` state before the cached call; and
- the difference in the state resulting from the call.
We store these because even if the cache hits,
we must update the state as if the call had been made.
Storing the difference suffices because the state increases monotonically.
See also `canUseCache`. -/
abbrev M :=
  ReaderT Context <| MonadCacheT ExprStructEq (Expr × Nat × Nat) <| StateRefT Nat MetaM

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

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

Разделы

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

Аффилиация

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