summaryrefslogtreecommitdiff
path: root/tests/fstar/arrays
diff options
context:
space:
mode:
authorSon Ho2024-03-20 06:17:41 +0100
committerSon Ho2024-03-20 06:17:41 +0100
commit5e99d127e0a746f5779779756fccf79f15c19d10 (patch)
tree6d10d613179568346e19cbc6bf95c6dd6897f574 /tests/fstar/arrays
parente6f002cfc1dfa41362bbb3a005c4261d09c52c58 (diff)
Regenerate the code
Diffstat (limited to 'tests/fstar/arrays')
-rw-r--r--tests/fstar/arrays/Arrays.Funs.fst10
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 15c82e93..731c7290 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -28,17 +28,17 @@ let array_to_mut_slice_
(** [arrays::array_len]:
Source: 'src/arrays.rs', lines 25:0-25:40 *)
let array_len (t : Type0) (s : array t 32) : result usize =
- let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i
+ let* s1 = array_to_slice t 32 s in Return (slice_len t s1)
(** [arrays::shared_array_len]:
Source: 'src/arrays.rs', lines 29:0-29:48 *)
let shared_array_len (t : Type0) (s : array t 32) : result usize =
- let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i
+ let* s1 = array_to_slice t 32 s in Return (slice_len t s1)
(** [arrays::shared_slice_len]:
Source: 'src/arrays.rs', lines 33:0-33:44 *)
let shared_slice_len (t : Type0) (s : slice t) : result usize =
- let i = slice_len t s in Return i
+ Return (slice_len t s)
(** [arrays::index_array_shared]:
Source: 'src/arrays.rs', lines 37:0-37:57 *)
@@ -268,8 +268,8 @@ let update_mut_slice (x : slice u32) : result (slice u32) =
let update_all : result unit =
let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in
let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in
- let* a = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in
- let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 a in
+ let* x = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in
+ let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 x in
let* s1 = update_mut_slice s in
let* _ = to_slice_mut_back s1 in
Return ()