summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
authorSon Ho2024-03-09 00:49:10 +0100
committerSon Ho2024-03-09 00:49:10 +0100
commit181749b50ef5f71e8639a5c2e97be99a6710e698 (patch)
tree53c93e14776510b59f44104e70621bb9d4c6a98b /tests/coq/misc
parent814f94b9e60818aac8060715e82edeffa6d5233f (diff)
Regenerate the test files
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/Loops.v64
1 files changed, 64 insertions, 0 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 8260db02..e235b60d 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -688,4 +688,68 @@ Definition list_nth_shared_mut_loop_pair_merge
Return (p1, back_'a)
.
+(** [loops::ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 345:0-345:56 *)
+Definition ignore_input_mut_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_mut_borrow_loop n i; Return _a
+.
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- incr_ignore_input_mut_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::incr_ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 353:0-353:60 *)
+Definition incr_ignore_input_mut_borrow
+ (n : nat) (a : u32) (i : u32) : result u32 :=
+ a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+.
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- ignore_input_shared_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_shared_borrow]:
+ Source: 'src/loops.rs', lines 362:0-362:59 *)
+Definition ignore_input_shared_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_shared_borrow_loop n i; Return _a
+.
+
End Loops.