aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml6
1 files changed, 6 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