diff options
author | Son Ho | 2023-12-23 00:59:55 +0100 |
---|---|---|
committer | Son Ho | 2023-12-23 00:59:55 +0100 |
commit | a4decc7654bc6f3301c0174124d21fdbc2dbc708 (patch) | |
tree | f992f3bb64609bf12d033a1424873a8134c66617 /tests/fstar/array | |
parent | ff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff) |
Regenerate the files
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/array/Array.Funs.fst | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst index da4164bc..4193ba7d 100644 --- a/tests/fstar/array/Array.Funs.fst +++ b/tests/fstar/array/Array.Funs.fst @@ -24,8 +24,7 @@ let array_to_mut_slice_ result ((slice t) & (slice t -> result (array t 32))) = let* (s1, to_slice_mut_back) = array_to_slice_mut t 32 s in - let back = fun ret -> to_slice_mut_back ret in - Return (s1, back) + Return (s1, to_slice_mut_back) (** [array::array_len]: Source: 'src/array.rs', lines 25:0-25:40 *) @@ -64,8 +63,7 @@ let index_mut_array result (t & (t -> result (array t 32))) = let* (x, index_mut_back) = array_index_mut_usize t 32 s i in - let back = fun ret -> index_mut_back ret in - Return (x, back) + Return (x, index_mut_back) (** [array::index_slice]: Source: 'src/array.rs', lines 56:0-56:46 *) @@ -79,8 +77,7 @@ let index_mut_slice result (t & (t -> result (slice t))) = let* (x, index_mut_back) = slice_index_mut_usize t s i in - let back = fun ret -> index_mut_back ret in - Return (x, back) + Return (x, index_mut_back) (** [array::slice_subslice_shared_]: Source: 'src/array.rs', lines 64:0-64:70 *) @@ -100,8 +97,7 @@ let slice_subslice_mut_ core_slice_index_Slice_index_mut u32 (core_ops_range_Range usize) (core_slice_index_SliceIndexRangeUsizeSliceTInst u32) x { start = y; end_ = z } in - let back = fun ret -> index_mut_back ret in - Return (s, back) + Return (s, index_mut_back) (** [array::array_to_slice_shared_]: Source: 'src/array.rs', lines 72:0-72:54 *) @@ -115,8 +111,7 @@ let array_to_slice_mut_ result ((slice u32) & (slice u32 -> result (array u32 32))) = let* (s, to_slice_mut_back) = array_to_slice_mut u32 32 x in - let back = fun ret -> to_slice_mut_back ret in - Return (s, back) + Return (s, to_slice_mut_back) (** [array::array_subslice_shared_]: Source: 'src/array.rs', lines 80:0-80:74 *) @@ -138,8 +133,7 @@ let array_subslice_mut_ (core_ops_index_IndexMutSliceTIInst u32 (core_ops_range_Range usize) (core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) x { start = y; end_ = z } in - let back = fun ret -> index_mut_back ret in - Return (s, back) + Return (s, index_mut_back) (** [array::index_slice_0]: Source: 'src/array.rs', lines 88:0-88:38 *) |