encoding — Mathlib

English

An encoding of bounded formulas as lists with decode/encode operations that are inverse.

Русский

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

LaTeX

$$$\\text{encoding}: \\text{Encoding}(\\Sigma n, L.BoundedFormula α n)$ with encode φ := φ.listEncode and decode l := (listDecode l)[0]?$$$

Lean4

/-- An encoding of bounded formulas as lists. -/
@[simps]
protected def encoding : Encoding (Σ n, L.BoundedFormula α n)
    where
  Γ := (Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ)
  encode φ := φ.2.listEncode
  decode l := (listDecode l)[0]?
  decode_encode
    φ := by
    have h := listDecode_encode_list [φ]
    rw [flatMap_singleton] at h
    rw [h]
    rfl

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