Function vstd::bytes::u16_from_le_bytes

source · 
pub exec fn u16_from_le_bytes(s: &[u8]) -> x : u16
Expand description
requires
s@.len() == 2,
ensures
x == spec_u16_from_le_bytes(s@),