summaryrefslogtreecommitdiff
path: root/tests/fstar-split/array/Array.Clauses.Template.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar-split/array/Array.Clauses.Template.fst')
-rw-r--r--tests/fstar-split/array/Array.Clauses.Template.fst21
1 files changed, 0 insertions, 21 deletions
diff --git a/tests/fstar-split/array/Array.Clauses.Template.fst b/tests/fstar-split/array/Array.Clauses.Template.fst
deleted file mode 100644
index b2f2649c..00000000
--- a/tests/fstar-split/array/Array.Clauses.Template.fst
+++ /dev/null
@@ -1,21 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [array]: templates for the decreases clauses *)
-module Array.Clauses.Template
-open Primitives
-open Array.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [array::sum]: decreases clause
- Source: 'src/array.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 *)
-unfold
-let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum1 : u32)
- (i : usize) : nat =
- admit ()
-