Rollup merge of #126468 - RalfJung:euclid, r=Mark-Simulacrum · model-checking/verify-rust-std@cd1c998 (original) (raw)

`@@ -2784,8 +2784,10 @@ macro_rules! int_impl {

`

2784

2784

`///

`

2785

2785

`` /// In other words, the result is self / rhs rounded to the integer q

``

2786

2786

`` /// such that self >= q * rhs.

``

2787

``

`` -

/// If self > 0, this is equal to round towards zero (the default in Rust);

``

2788

``

`` -

/// if self < 0, this is equal to round towards +/- infinity.

``

``

2787

`` +

/// If self > 0, this is equal to rounding towards zero (the default in Rust);

``

``

2788

`` +

/// if self < 0, this is equal to rounding away from zero (towards +/- infinity).

``

``

2789

`` +

/// If rhs > 0, this is equal to rounding towards -infinity;

``

``

2790

`` +

/// if rhs < 0, this is equal to rounding towards +infinity.

``

2789

2791

`///

`

2790

2792

`/// # Panics

`

2791

2793

`///

`

`@@ -2823,8 +2825,8 @@ macro_rules! int_impl {

`

2823

2825

`` /// Calculates the least nonnegative remainder of self (mod rhs).

``

2824

2826

`///

`

2825

2827

`/// This is done as if by the Euclidean division algorithm -- given

`

2826

``

`` -

/// r = self.rem_euclid(rhs), self = rhs * self.div_euclid(rhs) + r, and

``

2827

``

`` -

/// 0 <= r < abs(rhs).

``

``

2828

`` +

/// r = self.rem_euclid(rhs), the result satisfies

``

``

2829

`` +

/// self = rhs * self.div_euclid(rhs) + r and 0 <= r < abs(rhs).

``

2828

2830

`///

`

2829

2831

`/// # Panics

`

2830

2832

`///

`