:: [a] -> Int -> a 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.
Lookup function (safe). O(min n index).