Function extern_spec_Add_Wrapping_u64_Wrapping_u64_add 

pub fn extern_spec_Add_Wrapping_u64_Wrapping_u64_add(
    self_: Wrapping<u64>,
    rhs: Wrapping<u64>,
) -> Wrapping<u64>

extern spec for Wrapping<u64>::add

This is not a real function: its only use is for documentation.

ghost

ensures

result.0 == self.0 + rhs.0