aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/util.ml6
-rw-r--r--lib/util.mli6
2 files changed, 12 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index ad48e7981a..2711eee24a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1179,6 +1179,12 @@ let iterate_for a b f x =
let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
iterate a x
+(* Delayed computations *)
+
+type 'a delayed = unit -> 'a
+
+let delayed_force f = f ()
+
(* Misc *)
type ('a,'b) union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index f8fbc1f68c..bbef3462ad 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -291,6 +291,12 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
+(** {6 Delayed computations. } *)
+
+type 'a delayed = unit -> 'a
+
+val delayed_force : 'a delayed -> 'a
+
(** {6 Misc. } *)
type ('a,'b) union = Inl of 'a | Inr of 'b