library: list.FoldLeft and list.FoldRight now use HO

parent 3303fda9
......@@ -588,11 +588,7 @@ theory FoldLeft
use import List
type a
type b
function f b a : b
function fold_left (acc: b) (l: list a) : b =
function fold_left (f: 'b -> 'a -> b') (acc: 'b) (l: list 'a) : 'b =
match l with
| Nil -> acc
| Cons x r -> fold_left (f acc x) r
......@@ -604,11 +600,7 @@ theory FoldRight
use import List
type a
type b
function f a b : b
function fold_right (l: list a) (acc: b) : b =
function fold_right (f: 'a -> 'b -> b') (l: list 'a) (acc: 'b) : 'b =
match l with
| Nil -> acc
| Cons x r -> f x (fold_right r acc)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment