Skip to main content

_verus_external_fn_specification_4_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__32_V_32__62_

vstd::layout

Function _verus_external_fn_specification_4_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__32_V_32__62_ 

Source 
pub unsafe exec fn _verus_external_fn_specification_4_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__32_V_32__62_<V>() -> u : usize
Expand description
ensures
u as nat == size_of::<V>(),

Specification for core::mem::size_of::<V>