summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/Loops.Clauses.Template.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc/Loops.Clauses.Template.fst')
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst3
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index c8ed16f4..e43f8170 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -13,8 +13,7 @@ unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
(** [loops::sum_with_mut_borrows]: decreases clause
Source: 'src/loops.rs', lines 19:0-31:1 *)
unfold
-let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat
- =
+let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
admit ()
(** [loops::sum_with_shared_borrows]: decreases clause