Skip to main content

_verus_external_fn_specification_6_core_32__58__58__32_mem_32__58__58__32_size__of__val_32__58__58__32__60__32_V_32__62_

vstd::layout

Function _verus_external_fn_specification_6_core_32__58__58__32_mem_32__58__58__32_size__of__val_32__58__58__32__60__32_V_32__62_ 

Source 
pub unsafe exec fn _verus_external_fn_specification_6_core_32__58__58__32_mem_32__58__58__32_size__of__val_32__58__58__32__60__32_V_32__62_<V: ?Sized>(
    val: &V,
) -> u : usize
Expand description
ensures
u as nat == spec_size_of_val::<V>(val),

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