Function extern_spec_i16_checked_div 

pub fn extern_spec_i16_checked_div(self_: i16, rhs: i16) -> Option<i16>

extern spec for i16::checked_div

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

terminates

ghost

ensures

(result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1))

ensures

$type, +, checked_add, wrapping_add, saturating_add, overflowing_add, unchecked_add);
        spec_op_common!($type, -, checked_sub, wrapping_sub, saturating_sub, overflowing_sub, unchecked_sub);
        spec_op_common!($type, *, checked_mul, wrapping_mul, saturating_mul, overflowing_mul, unchecked_mul);

        extern_spec! {
            impl $type {
                #[allow(dead_code)]
                #[check(ghost)]
                #[ensures(result == -self)]
                fn wrapping_neg(self) -> $type;
            }
        }

        // Specify division separately, because it has the additional precondition that the divisor
        // is non-zero. Overflow on division can only occur on signed types and only when computing
        // `$type::MIN / -1`.
        extern_spec! {
            impl $type {
                #[allow(dead_code)]
                #[check(ghost)]
                // Returns `None` iff the divisor is zero or the division overflows
                #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
                // Else, returns the result of the division
                #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@