More uniformity between [CompletedNat] and [CompletedNatWitness].

src/CompletedNat.ml

@@ -20,6 +20,12 @@ let equal p1 p2 =
 let bottom =
   Infinity
 
+let epsilon =
+  Finite 0
+
+let singleton _ =
+  Finite 1
+
 let is_maximal p =
   match p with
   | Finite 0 ->
@@ -42,6 +48,13 @@ let min_lazy p1 p2 =
   | _ ->
       min p1 (Lazy.force p2)
 
+let until_finite p1 p2 =
+  match p1 with
+  | Finite _ ->
+      p1
+  | Infinity ->
+      Lazy.force p2
+
 let add p1 p2 =
   match p1, p2 with
   | Finite i1, Finite i2 ->

src/CompletedNat.mli

@@ -7,10 +7,15 @@ type t =
 
 include Fix.PROPERTY with type property = t
 
+val epsilon: t
+val singleton: 'a -> t
+
 val min: t -> t -> t
 val add: t -> t -> t
 
 val min_lazy: t -> t Lazy.t -> t
 val add_lazy: t -> t Lazy.t -> t
 
+val until_finite: t -> t Lazy.t -> t
+
 val print: t -> string