slice
container.abstract_array.slice
Precondition
Inherited from Sequence.slice
pre debug : from ≥ 0 debug : to = 0 || (if is_array_backed || debug_level > 1 then is_valid_index to-1 else true) debug : from <= to
Postcondition
Inherited from Sequence.slice
post debug: result.finite.is_yes_or_unknown debug: result.count = (to-from).as_i32
Type Parameters
0.095dev (GIT hash 5f19dac1008648f355e38b291a14980aecf8af80)
up to 'to' (excluded).
Complexity:
index access : O(1)
count : O(1)