module type Blob =
sig
(* Blob is the type for opaque leaves:
- * - checking equlity should be efficient
+ * - checking equality should be efficient
* - atoms have to be equipped with a total order relation
*)
type t
* *)
val pp : t -> string
- type input
- val embed : input -> t foterm
- (* saturate [proof] [type] -> [proof] * [type] *)
- val saturate : input -> input -> t foterm * t foterm
-
end