mt

Mathlib.Tactic.CC.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCState.mt

Lean4

/-- "Modification Time". The field `mt` is used to implement the mod-time optimization introduced by the
Simplify theorem prover. The basic idea is to introduce a counter `gmt` that records the number of
heuristic instantiation that have occurred in the current branch. It is incremented after each round
of heuristic instantiation. The field `mt` records the last time any proper descendant of this
entry was involved in a merge. -/
def mt (ccs : CCState) (e : Expr) : Nat :=
  match ccs.entries[e]? with
  | some n => n.mt
  | none => ccs.gmt

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

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

Разделы

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

Аффилиация

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