!! package:Agda

A variant of !! that might provide more informative error messages if the index is out of bounds. Precondition: The index should not be out of bounds.

xs !! n returns the element of the stream xs at index n. Note that the head of the stream has index 0. Beware: a negative or out-of-bounds index will cause an error.

Lookup function (safe). O(min n index).