mkSymmCongruencesKey

Mathlib.Tactic.CC.Addition

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

Lean4

/-- Return the `SymmCongruencesKey` associated with the equality `lhs = rhs`. -/
def mkSymmCongruencesKey (lhs rhs : Expr) : CCM SymmCongruencesKey := do
  let lhs ← getRoot lhs
  let rhs ← getRoot rhs
  if hash lhs > hash rhs then
    return { h₁ := rhs, h₂ := lhs }
  else
    return { h₁ := lhs, h₂ := rhs }

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

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

Разделы

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

Аффилиация

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