Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677#[allow(unused_imports)]use super::prelude::*;
verus! {
/// This function computes the minimum of two given integers.pub open spec fn min(x: int, y: int) -> int { if x <= y { x } else { y }}
/// This function computes the maximum of two given integers.pub open spec fn max(x: int, y: int) -> int { if x >= y { x } else { y }}
/// This function computes the maximum of three given integers.pub open spec fn max3(x: int, y: int, z: int) -> int { if x < y { max(y, z) } else { max(x, z) }}
/// This function converts the given integer `x` to a natural number/// by returning 0 when `x` is negative and `x` otherwise.pub open spec fn clip(x: int) -> nat { if x < 0 { 0 } else { x as nat }}
/// This function computes the absolute value of a given integer.pub open spec fn abs(x: int) -> nat { if x < 0 { -x as nat } else { x as nat }}
/// This function adds two integers together. It's sometimes/// useful as a substitute for `+` in triggers that feature/// function invocations, since mathematical operators can't be/// mixed with function invocations in triggers.pub open spec fn add(x: int, y: int) -> int { x + y}
/// This function subtracts two integers. It's sometimes useful as/// a substitute for `-` in triggers that feature function/// invocations, since mathematical operators can't be mixed with/// function invocations in triggers.pub open spec fn sub(x: int, y: int) -> int { x - y}
/// This function divides two integers. It's sometimes useful as a/// substitute for `/` in triggers that feature function/// invocations, since mathematical operators can't be mixed with/// function invocations in triggers.pub open spec fn div(x: int, y: int) -> int { x / y}
} // verus!