toArray

Mathlib.Lean.Meta.RefinedDiscrTree.Lookup

URI: https://scilib.ai/kg/mathlib#Lean.Meta.RefinedDiscrTree.MatchResult.toArray

Lean4

/-- Convert a `MatchResult` into a `Array`, with better matches at the start of the array.
-/
def toArray (mr : MatchResult α) : Array α :=
  mr.elts.foldr (init := #[]) fun _ a r => a.foldl (init := r) (· ++ ·)

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

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

Разделы

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

Аффилиация

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