findDefeq

Mathlib.Tactic.Linarith.Parsing

URI: https://scilib.ai/kg/mathlib#List.findDefeq

Lean4

/-- `findDefeq red m e` looks for a key in `m` that is defeq to `e` (up to transparency `red`),
and returns the value associated with this key if it exists.
Otherwise, it fails.
-/
def findDefeq {v : Type} (red : TransparencyMode) (m : List (Expr × v)) (e : Expr) : MetaM v := do
  if let some (_, n)← m.findM? fun ⟨e', _⟩ => withTransparency red (isDefEq e e') then
    return n
  else
    failure

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

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

Разделы

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

Аффилиация

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