diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 6 | ||||
| -rw-r--r-- | lib/util.mli | 6 |
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 |
