get

Mathlib.Tactic.Linarith.Datatypes

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

Lean4

/-- `l.get n` returns the value in `l` associated with key `n`, if it exists, and `none` otherwise.
This function assumes that `l` is sorted in decreasing order of the first argument,
that is, it will return `none` as soon as it finds a key smaller than `n`.
-/
def get (n : Nat) : Linexp → Option Int
  | [] => none
  | ((a, b) :: t) => if a < n then none else if a = n then some b else get n t

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

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

Разделы

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

Аффилиация

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