Bounded indices (Language Platform PRD §28.2 Numerics, LP-801).
`StdFin n` is a natural strictly below `n`, carried in the TYPE. An index
that cannot exist cannot be built, so an out-of-range access is not a
runtime error to handle: it is a program the checker rejects. The bound is
erased, so nothing here costs anything at runtime.
17constructor StdFinNextThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.