Skip to main content

_verus_external_fn_specification_7_core_32__58__58__32_mem_32__58__58__32_align__of__val_32__58__58__32__60__32_V_32__62_

vstd::layout

Function _verus_external_fn_specification_7_core_32__58__58__32_mem_32__58__58__32_align__of__val_32__58__58__32__60__32_V_32__62_ 

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

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