vstd
In vstd::
bytes
Functions
lemma_auto_spec_u128_to_from_le_bytes
lemma_auto_spec_u16_to_from_le_bytes
lemma_auto_spec_u32_to_from_le_bytes
lemma_auto_spec_u64_to_from_le_bytes
spec_u128_from_le_bytes
spec_u128_to_le_bytes
spec_u16_from_le_bytes
spec_u16_to_le_bytes
spec_u32_from_le_bytes
spec_u32_to_le_bytes
spec_u64_from_le_bytes
spec_u64_to_le_bytes
u128_from_le_bytes
u128_to_le_bytes
u16_from_le_bytes
u16_to_le_bytes
u32_from_le_bytes
u32_to_le_bytes
u64_from_le_bytes
u64_to_le_bytes
?
Settings
Function
vstd
::
bytes
::
u64_to_le_bytes
Copy item path
source
·
[
−
]
pub
exec
fn u64_to_le_bytes(x:
u64
) ->
s :
Vec
<
u8
>
Expand description
ensures
@ == spec_u64_to_le_bytes(x),
@.len() ==
8
,