Theorems · Theorem · logic and foundations

FirstOrder.Language.Term.listEncode.eq_def

∀ {L : FirstOrder.Language} {α : Type u'} (x : L.Term α),
  x.listEncode =
    match x with
    | FirstOrder.Language.var i => [Sum.inl i]
    | FirstOrder.Language.func f ts => Sum.inr ⟨l, f⟩ :: List.flatMap (fun i => (ts i).listEncode) (List.finRange l)

Defined in

Mathlib.ModelTheory.Encoding

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms