Std.Nat

Peano natural numbers for type-level computation.

Nat is intentionally small: it exists so indexed stdlib types can use a trusted, total unary natural-number index.

Types

# fn of_int(i: Int) -> Nat extern

Cast an Int to a Nat, clamping negatives to Z (== max(i, 0)). Even though Int is now inductive, it compiles to a native BEAM machine integer, so this cast is kept as an asserted FFI boundary against that native representation — exactly where Idris marks integerToNat total. It is the ONLY trusted step behind integer ranges; the enumeration itself (range_from) is genuine structural recursion.
# fn plus(m: Nat, n: Nat) -> Nat
# fn range_from(start: Int, count: Nat) -> List(Int)

Build [start, start + 1, …, start + count - 1], driven by a structural Nat fuel. The recursion is on count, so it is certified terminating.
# fn range_upto(from: Int, to: Int) -> List(Int)

Exclusive integer range a..b = [a, …, b - 1]; empty when a >= b (of_int clamps the negative gap to Z). The surface a..b desugars here.
# fn range_upto_incl(from: Int, to: Int) -> List(Int)

Inclusive integer range a..=b = [a, …, b]. The surface a..=b desugars here.
# fn to_integer(value: Nat) -> Int

Project a natural number to a machine integer (structural, total; the constructive inverse of the trusted of_int clamp — this direction needs no assertion because Nat is well-founded).