vstd::bytes

Function spec_u64_to_le_bytes_to_open

Source 
pub proof fn spec_u64_to_le_bytes_to_open(x: u64)
Expand description
ensures
spec_u64_to_le_bytes(x) == spec_u64_to_le_bytes_open(x),