diff options
Diffstat (limited to 'hol-light/TacticRecording/lib.ml')
| -rw-r--r-- | hol-light/TacticRecording/lib.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml index b1309f84..5de28331 100644 --- a/hol-light/TacticRecording/lib.ml +++ b/hol-light/TacticRecording/lib.ml @@ -19,6 +19,15 @@ let rec foldr f xs a = | [] -> a;; +(* foldr1 : ('a -> 'a -> 'a) -> 'a list -> 'a *) + +let rec foldr1 f xs = + match xs with + x::[] -> x + | x1::xs2 -> f x1 (foldr1 f xs2) + | [] -> failwith "foldr1: Empty list";; + + (* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b *) let rec foldl f a xs = |