summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
authorSon Ho2023-01-06 01:10:51 +0100
committerSon HO2023-02-03 11:21:46 +0100
commita2e52dd8e4f53600c74744026aeae15d99d104b0 (patch)
treead5c81fd1e9763955d1c8250d3dc730f39f678d5 /tests/coq/misc
parent852ee63cb876d419d4830eb5192604d58b07b495 (diff)
Fix an issue with the translation of loops::clear
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/Loops.v8
1 files changed, 3 insertions, 5 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ec8fa39c..29f312bf 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -63,7 +63,7 @@ Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
.
(** [loops::clear] *)
-Definition clear_loop_fwd_back
+Fixpoint clear_loop_fwd_back
(n : nat) (v : vec u32) (i : usize) : result (vec u32) :=
match n with
| O => Fail_ OutOfFuel
@@ -73,16 +73,14 @@ Definition clear_loop_fwd_back
then (
i1 <- usize_add i 1%usize;
v0 <- vec_index_mut_back u32 v i (0%u32);
- v1 <- clear_loop_fwd n0 v0 i1;
- let _ := v1 in
- Return v0)
+ clear_loop_fwd_back n0 v0 i1)
else Return v
end
.
(** [loops::clear] *)
Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) :=
- v0 <- clear_loop_fwd n v (0%usize); let _ := v0 in Return v
+ clear_loop_fwd_back n v (0%usize)
.
(** [loops::List] *)