type t
val eq : t -> t -> bool
val compare : t -> t -> int
- val eqP : t
+ val eqP : unit -> t
(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
type input
val embed : input -> t foterm
(* saturate [proof] [type] -> [proof] * [type] *)
- val saturate : input -> input -> t foterm * t foterm
+ (* val saturate : input -> input -> t foterm * t foterm *)
end