diff options
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index fa21cd83ed..3b5c90b020 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -857,6 +857,13 @@ let rec prlist elem l = match l with | [] -> mt () | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t) +(* unlike all other functions below, [prlist] works lazily. + if a strict behavior is needed, use [prlist_strict] instead. *) + +let rec prlist_strict elem l = match l with + | [] -> mt () + | h::t -> (elem h)++(prlist_strict elem t) + let rec prlist_with_sep sep elem l = match l with | [] -> mt () | [h] -> elem h |