Module Common.LogicSource

Sourcemodule type LRA_REIFICATION = sig ... end
Sourcetype z =
  1. | Z
Sourcetype 'a s =
  1. | S
Sourcetype ('a, _) op =
  1. | True : 'a -> ('a, z) op
  2. | False : 'a -> ('a, z) op
  3. | Zero : 'a -> ('a, z) op
  4. | Succ : 'a -> ('a, z s) op
  5. | Minus : 'a -> ('a, z s) op
  6. | Eq : 'a -> ('a, z s s) op
  7. | Max : 'a -> ('a, z s s) op
  8. | IMax : 'a -> ('a, z s s) op
  9. | Le : 'a -> ('a, z s s) op
  10. | Ite : 'a -> ('a, z s s s) op
Sourcetype ('a, 'b) arrow =
  1. | Zero : 'b -> (z, 'b) arrow
  2. | One : ('b -> 'b) -> (z s, 'b) arrow
  3. | Two : ('b -> 'b -> 'b) -> (z s s, 'b) arrow
  4. | Three : ('b -> 'b -> 'b -> 'b) -> (z s s s, 'b) arrow
Sourcetype ('a, 'c) k = {
  1. mk : 'b. ('a, 'b) op -> ('b, 'c) arrow;
}
Sourcemodule type LRA_SPECIFICATION = sig ... end
Sourcetype theory = (Universes.pred * bool) list
Sourcemodule type QFUF_SPECIFICATION = sig ... end