package universo

  1. Overview
  2. Docs
module B = Kernel.Basic
module T = Kernel.Term
module type LRA_REIFICATION = sig ... end
type z =
  1. | Z
type 'a s =
  1. | S
type ('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
type ('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
type ('a, 'c) k = {
  1. mk : 'b. ('a, 'b) op -> ('b, 'c) arrow;
}
module type LRA_SPECIFICATION = sig ... end
type theory = (Universes.pred * bool) list
module type QFUF_SPECIFICATION = sig ... end