listEncode — Mathlib

English

Encodes a bounded formula as a list of symbols, separating variables and function symbols.

Русский

Кодирует ограниченную формулу как список символов, разделяя переменные и символьные функции.

LaTeX

$$$\text{listEncode}: L.BoundedFormula α n \to \text{List}((Σ k, L.Term (α ⊕ \! Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ))$$$

Lean4

/-- Encodes a term as a list of variables and function symbols. -/
def listEncode : L.Term α → List (α ⊕ (Σ i, L.Functions i))
  | var i => [Sum.inl i]
  | func f ts => Sum.inr (⟨_, f⟩ : Σ i, L.Functions i) :: (List.finRange _).flatMap fun i => (ts i).listEncode

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