summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2024-02-03 00:00:36 +0100
committerSon Ho2024-02-03 00:00:36 +0100
commit9cc912e2414870df85ffc4dd346ade5dba2b5c37 (patch)
tree1d8290e4b947e431c3d8d3a9f8575f23c3afe5e1 /tests
parent3157013edd4d0e70a5c6fb8a5b236043865adbe0 (diff)
Fix minor issues
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 =