- axL {L : Language} {k : ℕ} (r : L.Rel k) (v : Fin k → SyntacticTerm L) : Code L
- verum {L : Language} : Code L
- and {L : Language} : SyntacticFormula L → SyntacticFormula L → Code L
- or {L : Language} : SyntacticFormula L → SyntacticFormula L → Code L
- all {L : Language} : SyntacticSemiformula L 1 → Code L
- ex {L : Language} : SyntacticSemiformula L 1 → SyntacticTerm L → Code L
- id {L : Language} : SyntacticFormula L → Code L
Instances For
def
LO.FirstOrder.System.Code.equiv
(L : Language)
:
Code L ≃ (k : ℕ) × L.Rel k × (Fin k → SyntacticTerm L) ⊕ Unit ⊕ SyntacticFormula L × SyntacticFormula L ⊕ SyntacticFormula L × SyntacticFormula L ⊕ SyntacticSemiformula L 1 ⊕ SyntacticSemiformula L 1 × SyntacticTerm L ⊕ SyntacticFormula L
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.FirstOrder.System.instEncodableCodeOfDecidableEqOfFuncOfRel
{L : Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
:
Equations
- One or more equations did not get rendered due to their size.