The element at a position, as an option: an index past the end is absent,
never an error and never a wrong element.
275def stdListIndex =
276 (lambda erased element : Type 0 .
277 (lambda unrestricted values : (family StdList element) .
278 (lambda unrestricted position : Nat .
279 (app
280 (eliminate
281 StdList
282 (lambda unrestricted current : (family StdList element) .
283 (pi unrestricted remaining : Nat . (family StdOption element)))
284 values
285 (branch
286 StdListEmpty
287 .
288 (lambda unrestricted remaining : Nat . (constructor StdOption StdNone element)))
289 (branch
290 StdListCons
291 head
292 tail
293 induction
294 .
295 (lambda unrestricted remaining : Nat .
296 (nat-eliminate
297 (lambda unrestricted current : Nat . (family StdOption element))
298 (constructor StdOption StdSome element head)
299 (lambda unrestricted predecessor : Nat .
300 (lambda unrestricted inner : (family StdOption element) .
301 (induction predecessor)))
302 remaining))))
303 position))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.