listDecode — Mathlib

English

Decodes a list back into a list of L-terms by reconstructing variables and function applications.

Русский

Декодирует список обратно в список термов, восстанавливая переменные и применения функций.

LaTeX

$$$\text{listDecode}: \text{List}((α \oplus (Σ i, L.Functions i))) \to \text{List}(L.Term α)$$$

Lean4

/-- Decodes a list of variables and function symbols as a list of terms. -/
def listDecode : List (α ⊕ (Σ i, L.Functions i)) → List (L.Term α)
  | [] => []
  | Sum.inl a :: l => (var a) :: listDecode l
  | Sum.inr ⟨n, f⟩ :: l =>
    if h : n ≤ (listDecode l).length then (func f (fun i => (listDecode l)[i])) :: (listDecode l).drop n else []

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