summaryrefslogtreecommitdiff
path: root/tests/fstar-split/arrays/Arrays.Clauses.Template.fst
diff options
context:
space:
mode:
authorSon Ho2024-02-02 23:33:20 +0100
committerSon Ho2024-02-02 23:33:20 +0100
commit7ecf28dc36f724a4ab4b3b4976421e4e4c397f3b (patch)
treead9f8cfb3c035fb86623d83d24e5590bb7bbd8a4 /tests/fstar-split/arrays/Arrays.Clauses.Template.fst
parent5cf7d9c0d6b0bc77f2219e7b8b29badce26d51e8 (diff)
Rename and regenerate some files
Diffstat (limited to '')
-rw-r--r--tests/fstar-split/arrays/Arrays.Clauses.Template.fst (renamed from tests/fstar-split/array/Array.Clauses.Template.fst)14
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/fstar-split/array/Array.Clauses.Template.fst b/tests/fstar-split/arrays/Arrays.Clauses.Template.fst
index b2f2649c..8cc32583 100644
--- a/tests/fstar-split/array/Array.Clauses.Template.fst
+++ b/tests/fstar-split/arrays/Arrays.Clauses.Template.fst
@@ -1,19 +1,19 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [array]: templates for the decreases clauses *)
-module Array.Clauses.Template
+(** [arrays]: templates for the decreases clauses *)
+module Arrays.Clauses.Template
open Primitives
-open Array.Types
+open Arrays.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [array::sum]: decreases clause
- Source: 'src/array.rs', lines 242:0-250:1 *)
+(** [arrays::sum]: decreases clause
+ Source: 'src/arrays.rs', lines 242:0-250:1 *)
unfold
let sum_loop_decreases (s : slice u32) (sum1 : u32) (i : usize) : nat =
admit ()
-(** [array::sum2]: decreases clause
- Source: 'src/array.rs', lines 252:0-261:1 *)
+(** [arrays::sum2]: decreases clause
+ Source: 'src/arrays.rs', lines 252:0-261:1 *)
unfold
let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum1 : u32)
(i : usize) : nat =