The element at a position, as an option: an index past the end is absent,
never an error and never a wrong element.
220def stdListIndex =
221 (lambda erased element : Type 0 .
222 (lambda unrestricted values : (family StdList element) .
223 (lambda unrestricted position : Nat .
224 (app
225 (eliminate
226 StdList
227 (lambda unrestricted current : (family StdList element) .
228 (pi unrestricted remaining : Nat . (family StdOption element)))
229 values
230 (branch
231 StdListEmpty
232 .
233 (lambda unrestricted remaining : Nat . (constructor StdOption StdNone element)))
234 (branch
235 StdListCons
236 head
237 tail
238 induction
239 .
240 (lambda unrestricted remaining : Nat .
241 (nat-eliminate
242 (lambda unrestricted current : Nat . (family StdOption element))
243 (constructor StdOption StdSome element head)
244 (lambda unrestricted predecessor : Nat .
245 (lambda unrestricted inner : (family StdOption element) .
246 (induction predecessor)))
247 remaining))))
248 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.