vstd::bytes

Function spec_u64_to_le_bytes_open

Source 
pub open spec fn spec_u64_to_le_bytes_open(x: u64) -> Seq<u8>
Expand description
{
    #[verusfmt::skip]
    seq![
        (x & 0xff) as u8, ((x >> 8) & 0xff) as u8, ((x >> 16) & 0xff) as u8, ((x >> 24) &
        0xff) as u8, ((x >> 32) & 0xff) as u8, ((x >> 40) & 0xff) as u8, ((x >> 48) &
        0xff) as u8, ((x >> 56) & 0xff) as u8,
    ]
}