A list of the naturals below a bound, in increasing order: `[0, 1, ..., n-1]`.
306def stdListNaturalsBelow =
307 (lambda unrestricted bound : Nat .
308 (nat-eliminate
309 (lambda unrestricted current : Nat . (family StdList Nat))
310 (constructor StdList StdListEmpty Nat)
311 (lambda unrestricted predecessor : Nat .
312 (lambda unrestricted induction : (family StdList Nat) .
313 (stdListAppend
314 Nat
315 induction
316 (constructor StdList StdListCons Nat predecessor (constructor StdList StdListEmpty Nat)))))
317 bound))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.