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