summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar-split/arrays/Arrays.Clauses.fst10
-rw-r--r--tests/fstar/arrays/Arrays.Clauses.fst10
2 files changed, 10 insertions, 10 deletions
diff --git a/tests/fstar-split/arrays/Arrays.Clauses.fst b/tests/fstar-split/arrays/Arrays.Clauses.fst
index 68cbf216..aca328c2 100644
--- a/tests/fstar-split/arrays/Arrays.Clauses.fst
+++ b/tests/fstar-split/arrays/Arrays.Clauses.fst
@@ -1,17 +1,17 @@
-(** [array]: decreases clauses *)
-module Array.Clauses
+(** [arrays]: decreases clauses *)
+module Arrays.Clauses
open Primitives
-open Array.Types
+open Arrays.Types
open FStar.List.Tot
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [array::sum]: decreases clause *)
+(** [arrays::sum]: decreases clause *)
unfold
let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat =
if i < length s then length s - i else 0
-(** [array::sum2]: decreases clause *)
+(** [arrays::sum2]: decreases clause *)
unfold
let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32)
(i : usize) : nat =
diff --git a/tests/fstar/arrays/Arrays.Clauses.fst b/tests/fstar/arrays/Arrays.Clauses.fst
index 68cbf216..aca328c2 100644
--- a/tests/fstar/arrays/Arrays.Clauses.fst
+++ b/tests/fstar/arrays/Arrays.Clauses.fst
@@ -1,17 +1,17 @@
-(** [array]: decreases clauses *)
-module Array.Clauses
+(** [arrays]: decreases clauses *)
+module Arrays.Clauses
open Primitives
-open Array.Types
+open Arrays.Types
open FStar.List.Tot
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [array::sum]: decreases clause *)
+(** [arrays::sum]: decreases clause *)
unfold
let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat =
if i < length s then length s - i else 0
-(** [array::sum2]: decreases clause *)
+(** [arrays::sum2]: decreases clause *)
unfold
let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32)
(i : usize) : nat =