English
There is an encodable instance for L.Term α constructed from encodable α and encodable (Σ i, L.Functions i).
Русский
Существует инстанс кодируемости для L.Term α, построенный из кодируемости α и кодируемости (Σ i, L.Functions i).
LaTeX
$$instance [Encodable α] [Encodable (Σ i, L.Functions i)] : Encodable (L.Term α)$$
Lean4
/-- Encodes a bounded formula as a list of symbols. -/
def listEncode : ∀ {n : ℕ}, L.BoundedFormula α n → List ((Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ))
| n, falsum => [Sum.inr (Sum.inr (n + 2))]
| _, equal t₁ t₂ => [Sum.inl ⟨_, t₁⟩, Sum.inl ⟨_, t₂⟩]
| n, rel R ts => [Sum.inr (Sum.inl ⟨_, R⟩), Sum.inr (Sum.inr n)] ++ (List.finRange _).map fun i => Sum.inl ⟨n, ts i⟩
| _, imp φ₁ φ₂ => (Sum.inr (Sum.inr 0) :: φ₁.listEncode) ++ φ₂.listEncode
| _, all φ => Sum.inr (Sum.inr 1) :: φ.listEncode
