Commit c361c72a authored by Mário Pereira's avatar Mário Pereira

Cosmetic in mach.array.Array63; defined fold_left for sequences.

parent 2d0cdc13
......@@ -257,8 +257,7 @@ module Array63
requires { 0 <= ofs /\ 0 <= len }
requires { ofs + len <= a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < len ->
result[i] = a[ofs + i] }
ensures { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
val copy (a: array 'a) : array 'a
ensures { result.length = a.length }
......
......@@ -542,15 +542,10 @@ theory FoldLeft
use import Seq
use import int.Int
function fold ('b -> 'a -> 'b) 'b (seq 'a) int : 'b
axiom fold_stop: forall f: 'b -> 'a -> 'b, acc: 'b, s: seq 'a, i: int.
i >= length s -> fold f acc s i = acc
axiom fold_loop: forall f: 'b -> 'a -> 'b, acc: 'b, s: seq 'a, i: int.
i < length s -> fold f acc s i = fold f (f acc s[i]) s (i+1)
function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (s: seq 'a) : 'b =
fold f acc s 0
let rec function fold_left (f: 'a -> 'b -> 'a) (acc: 'a) (s: seq 'b) : 'a
variant { length s }
= if length s = 0 then acc
else fold_left f (f acc s[0]) s[1 ..]
use import list.List
use import OfList
......
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