You can search for identifiers within the package.
in-package search v0.2.0
universo.common
Common.Logic
module B = Kernel.Basic
module T = Kernel.Term
module type LRA_REIFICATION = sig ... end
type z =
| Z
type 'a s =
| S
type ('a, _) op =
| True : 'a -> ('a, z) op
| False : 'a -> ('a, z) op
| Zero : 'a -> ('a, z) op
| Succ : 'a -> ('a, z s) op
| Minus : 'a -> ('a, z s) op
| Eq : 'a -> ('a, z s s) op
| Max : 'a -> ('a, z s s) op
| IMax : 'a -> ('a, z s s) op
| Le : 'a -> ('a, z s s) op
| Ite : 'a -> ('a, z s s s) op
type ('a, 'b) arrow =
| Zero : 'b -> (z, 'b) arrow
| One : ('b -> 'b) -> (z s, 'b) arrow
| Two : ('b -> 'b -> 'b) -> (z s s, 'b) arrow
| Three : ('b -> 'b -> 'b -> 'b) -> (z s s s, 'b) arrow
type ('a, 'c) k = {
mk : 'b. ('a, 'b) op -> ('b, 'c) arrow;
}
module type LRA_SPECIFICATION = sig ... end
module MakeLraSpecif (Lra : LRA_REIFICATION) : LRA_SPECIFICATION
type theory = (Universes.pred * bool) list
module type QFUF_SPECIFICATION = sig ... end