partitionByType

Mathlib.Tactic.Linarith.Frontend

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.partitionByType

Lean4

/-- `partitionByType l` takes a list `l` of proofs of comparisons. It sorts these proofs by
the type of the variables in the comparison, e.g. `(a : ℚ) < 1` and `(b : ℤ) > c` will be separated.
Returns a map from a type to a list of comparisons over that type.
-/
def partitionByType (l : List Expr) : MetaM (ExprMultiMap Expr) :=
  l.foldlM
    (fun m h => do
      m.insert (← typeOfIneqProof h) h)
    #[]

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

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

Разделы

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

Аффилиация

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