Function level_is_in_range Copy item path

pub open spec fn level_is_in_range(level: int) -> bool

{ 1 <= level <= NR_LEVELS() as int }