def
LO.FirstOrder.UTerm.encodable
{L : LO.FirstOrder.Language}
{μ : Type v}
[(k : ℕ) → Encodable (L.Func k)]
[Encodable μ]
:
Encodable (LO.FirstOrder.UTerm L μ)
Equations
- LO.FirstOrder.UTerm.encodable = Encodable.ofEquiv (WType (LO.FirstOrder.UTerm.Edge L μ)) (LO.FirstOrder.UTerm.equivW L μ)
Instances For
def
LO.FirstOrder.Semiterm.encodable
{L : LO.FirstOrder.Language}
{μ : Type v}
[(k : ℕ) → Encodable (L.Func k)]
[Encodable μ]
{n : ℕ}
:
Encodable (LO.FirstOrder.Semiterm L μ n)
Equations
- LO.FirstOrder.Semiterm.encodable = Encodable.ofEquiv { t : LO.FirstOrder.UTerm L μ // t.bv ≤ n } LO.FirstOrder.UTerm.subtEquiv
Instances For
def
LO.FirstOrder.UFormula.encodable
{L : LO.FirstOrder.Language}
{μ : Type v}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
[Encodable μ]
:
Equations
- LO.FirstOrder.UFormula.encodable = Encodable.ofEquiv (WType (LO.FirstOrder.UFormula.Edge L μ)) (LO.FirstOrder.UFormula.equivW L μ)
Instances For
def
LO.FirstOrder.Semiformula.encodable
{L : LO.FirstOrder.Language}
{μ : Type v}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
[Encodable μ]
{n : ℕ}
:
Encodable (LO.FirstOrder.Semiformula L μ n)
Equations
- LO.FirstOrder.Semiformula.encodable = Encodable.ofEquiv { p : LO.FirstOrder.UFormula L μ // p.bv ≤ n } LO.FirstOrder.UFormula.subfEquiv