size_of_facts

Function size_of_facts 

Source
pub broadcast proof fn size_of_facts()
Expand description
ensures
#[trigger] size_of::<u8>() == 1,
#[trigger] size_of::<u16>() == 2,
#[trigger] size_of::<u32>() == 4,
#[trigger] size_of::<u64>() == 8,
#[trigger] size_of::<usize>() == 8,

Proof that the size of the unsigned integer types is as expected.