Commit 5774a161 authored by Andrei Paskevich's avatar Andrei Paskevich

replace unnecessary "clone" by "use" in array.mlw

parent 088a76ba
...@@ -138,7 +138,7 @@ module ArrayPermut ...@@ -138,7 +138,7 @@ module ArrayPermut
use import int.Int use import int.Int
use import Array use import Array
clone import map.MapPermut as M use import map.MapPermut as M
predicate exchange (a1 a2: array 'a) (i j: int) = predicate exchange (a1 a2: array 'a) (i j: int) =
M.exchange a1.elts a2.elts i j M.exchange a1.elts a2.elts i j
...@@ -180,7 +180,7 @@ end ...@@ -180,7 +180,7 @@ end
module ArraySum module ArraySum
use import Array use import Array
clone import map.MapSum as M use import map.MapSum as M
(** [sum a l h] is the sum of [a[i]] for [l <= i < h] *) (** [sum a l h] is the sum of [a[i]] for [l <= i < h] *)
function sum (a: array int) (l h: int) : int = M.sum a.elts l h function sum (a: array int) (l h: int) : int = M.sum a.elts l h
......
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