Module Axiom


module Axiom: sig .. end

Representations of Moca equations




type side =
| Left
| Right

type axiom =
| Com of Symb.symbol
| Ass of Symb.symbol
| Nil of Symb.symbol * Symb.symbol
| Idem of Symb.symbol
| Neu of side * Symb.symbol * Symb.symbol
| Abs of side * Symb.symbol * Symb.symbol
| Inv of side * Symb.symbol * Symb.symbol * Symb.symbol
| Dis of side * Symb.symbol * Symb.symbol
| InvDis of side * Symb.symbol * Symb.symbol
| UDis of Symb.symbol * Symb.symbol * Symb.symbol
| Invol of Symb.symbol
| UNil of Symb.symbol * Symb.symbol
| UIdem of Symb.symbol
| InvNeu of Symb.symbol * Symb.symbol * Symb.symbol
type theory = axiom list 
val com : Symb.symbol -> theory
val ass : Symb.symbol -> theory
val nil : Symb.symbol -> Symb.symbol -> theory
val idem : Symb.symbol -> theory
val lneu : Symb.symbol -> Symb.symbol -> theory
val rneu : Symb.symbol -> Symb.symbol -> theory
val neu : Symb.symbol -> Symb.symbol -> theory
val labs : Symb.symbol -> Symb.symbol -> theory
val rabs : Symb.symbol -> Symb.symbol -> theory
val abs : Symb.symbol -> Symb.symbol -> theory
val linv : Symb.symbol -> Symb.symbol -> Symb.symbol -> theory
val rinv : Symb.symbol -> Symb.symbol -> Symb.symbol -> theory
val inv : Symb.symbol -> Symb.symbol -> Symb.symbol -> theory
val ldis : Symb.symbol -> Symb.symbol -> theory
val rdis : Symb.symbol -> Symb.symbol -> theory
val dis : Symb.symbol -> Symb.symbol -> theory
val linvdis : Symb.symbol -> Symb.symbol -> theory
val rinvdis : Symb.symbol -> Symb.symbol -> theory
val invdis : Symb.symbol -> Symb.symbol -> theory
val udis : Symb.symbol -> Symb.symbol -> Symb.symbol -> theory
val invol : Symb.symbol -> theory
val unil : Symb.symbol -> Symb.symbol -> theory
val uidem : Symb.symbol -> theory
val invneu : Symb.symbol -> Symb.symbol -> Symb.symbol -> theory
val eqnset_of_theory : theory -> Equation.EqnSet.t