A list of the naturals below a bound, in increasing order: `[0, 1, ..., n-1]`.
251def stdListNaturalsBelow =
252 (lambda unrestricted bound : Nat .
253 (nat-eliminate
254 (lambda unrestricted current : Nat . (family StdList Nat))
255 (constructor StdList StdListEmpty Nat)
256 (lambda unrestricted predecessor : Nat .
257 (lambda unrestricted induction : (family StdList Nat) .
258 (stdListAppend
259 Nat
260 induction
261 (constructor StdList StdListCons Nat predecessor (constructor StdList StdListEmpty Nat)))))
262 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.