Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.listEncode

{L : FirstOrder.Language} →
  {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)

Encodes a bounded formula as a list of symbols.

Defined in

Mathlib.ModelTheory.Encoding

Cited by

4 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms