Function index_is_in_range Copy item path

pub open spec fn index_is_in_range(index: int) -> bool

{ 0 <= index < NR_ENTRIES() }