Skip to main content

integer_in_range

Function integer_in_range 

Source
pub open spec fn integer_in_range<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64>(
    value: int,
) -> bool
Expand description
{
    &&& (HAS_MIN ==> MIN as int <= value)
    &&& (HAS_MAX ==> value <= MAX as int)

}