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.098dev (GIT hash b44352b4c68decbc58a097b291a1c8f3a5a05486)
up to 'to' (excluded).
Complexity:
index access : O(1)
count : O(1)