From 57af3d9556dc978c0bd6f57aa0c288eaf71c10b5 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Wed, 3 Aug 2011 17:21:28 +0200 Subject: [PATCH] list: theories FoldLeft and FoldRight --- theories/list.why | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/theories/list.why b/theories/list.why index e431aeebb..1adc1f141 100644 --- a/theories/list.why +++ b/theories/list.why @@ -15,7 +15,7 @@ theory Length | Cons _ r -> 1 + length r end - lemma Length_nonnegative: forall l: list 'a. length(l) >= 0 + lemma Length_nonnegative: forall l: list 'a. length l >= 0 lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil @@ -246,16 +246,39 @@ theory Map type b function f a : b - function map(l: list a) : list b = + function map (l: list a) : list b = match l with | Nil -> Nil | Cons x r -> Cons (f x) (map r) end +end + +theory FoldLeft + use import List + + type a + type b + function f b a : b + function fold_left (acc: b) (l: list a) : b = + match l with + | Nil -> acc + | Cons x r -> fold_left (f acc x) r + end end -theory Fold - (* TODO (a la Map) *) +theory FoldRight + use import List + + type a + type b + function f a b : b + + function fold_right (l: list a) (acc: b) : b = + match l with + | Nil -> acc + | Cons x r -> f x (fold_right r acc) + end end theory ListRich -- GitLab