find?

Mathlib.Tactic.Explode.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Explode.Entries.find?

Lean4

/-- Find a row where `Entry.expr` == `e`. -/
def find? (es : Entries) (e : Expr) : Option Entry :=
  es.s[e]?

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

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

Разделы

Аффилиация

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