addACEq

Mathlib.Tactic.CC.Addition

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCM.addACEq

Lean4

/-- Given AC variables `e₁` and `e₂` which are in the same equivalence class, add the proof of
`e₁ = e₂` to the AC module. -/
def addACEq (e₁ e₂ : Expr) : CCM Unit := do
  dbgTraceACEq "cc eq:" e₁ e₂
  modifyACTodo fun acTodo => acTodo.push (e₁, e₂, .eqProof e₁ e₂)
  processAC
  dbgTraceACState

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

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

Разделы

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

Аффилиация

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