flatten

Mathlib.Lean.Meta.RefinedDiscrTree.Lookup

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

Lean4

/-- Convert a `MatchResult` into an `Array` of `Array`s. Each `Array` corresponds to one pattern.
The better matching patterns are at the start of the outer array.
For each inner array, the entries are ordered in the order they were inserted.
-/
def flatten (mr : MatchResult α) : Array (Array α) :=
  mr.elts.foldr (init := #[])
    (fun _ arr cand => cand ++ arr)
      /-
      A partial match captures the intermediate state of a match execution.

      N.B. Discrimination tree matching has non-determinism due to stars,
      so the matching loop maintains a stack of partial match results.
      -/

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

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

Разделы

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

Аффилиация

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