Theorems · Theorem · logic and foundations

FirstOrder.Language.Term.constantsToVars.eq_def

∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (x : (L.withConstants γ).Term α),
  x.constantsToVars =
    match x with
    | FirstOrder.Language.var a => FirstOrder.Language.var (Sum.inr a)
    | FirstOrder.Language.func f ts =>
      Sum.casesOn f (fun f => FirstOrder.Language.func f fun i => (ts i).constantsToVars) fun c =>
        FirstOrder.Language.var (Sum.inl c)
    | FirstOrder.Language.func f ts =>
      Sum.casesOn f (fun f => FirstOrder.Language.func f fun i => (ts i).constantsToVars) fun c => isEmptyElim c

Defined in

Mathlib.ModelTheory.Syntax

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms