Raise the index by m and weaken the bound by m, adding m to the left-hand side of n.

Raise the index by m and weaken the bound by m, adding m to the right-hand side of n.

Weaken the bound, replacing it by another number greater than or equal to itself. This does not change the index.

Weaken the bound by m, adding it to the left-hand side of the existing bound. This does not change the index.

Unboxed variant of weakenL.

Weaken the bound by m, adding it to the right-hand side of the existing bound. This does not change the index.

Unboxed variant of weakenR.

Return the successor of the Fin or return nothing if the argument is the greatest inhabitant.

Variant of succ for unlifted finite numbers.

Fold over the numbers bounded by n in ascending order. This is lazy in the accumulator.

ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))

Strict fold over the numbers bounded by n in ascending order. For convenince, this differs from foldl' in the order of the parameters.

ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))

Generalization of ascend' that lets the caller pick the starting index:

ascend' === ascendFrom' 0

Variant of ascendFrom' with unboxed arguments.

Strict monadic left fold over the numbers bounded by n in ascending order. Roughly:

ascendM 4 z0 f =
  f 0 z0 >>= \z1 ->
  f 1 z1 >>= \z2 ->
  f 2 z2 >>= \z3 ->
  f 3 z3

Variant of ascendM that takes an unboxed Nat and provides an unboxed Fin to the callback.

Monadic traversal of the numbers bounded by n in ascending order.

ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3

Variant of ascendM_ that takes an unboxed Nat and provides an unboxed Fin to the callback.

Fold over the numbers bounded by n in descending order. This is lazy in the accumulator. For convenince, this differs from foldr in the order of the parameters.

descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))

Fold over the numbers bounded by n in descending order. This is strict in the accumulator. For convenince, this differs from foldr' in the order of the parameters.

descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))

Strict monadic left fold over the numbers bounded by n in descending order. Roughly:

descendM 4 z f =
  f 3 z0 >>= \z1 ->
  f 2 z1 >>= \z2 ->
  f 1 z2 >>= \z3 ->
  f 0 z3

Monadic traversal of the numbers bounded by n in descending order.

descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0

Generate all values of a finite set in ascending order.

>>> ascending (Nat.constant @3)
[Fin 0,Fin 1,Fin 2]

Generate all values of a finite set in descending order.

>>> descending (Nat.constant @3)
[Fin 2,Fin 1,Fin 0]

Generate len values starting from off in ascending order.

>>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)
[Fin 2,Fin 3,Fin 4]

Generate len values starting from 'off + len - 1' in descending order.

>>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
[Fin 4,Fin 3,Fin 2]

A finite set of no values is impossible.

Extract the Int from a 'Fin n'. This is intended to be used at a boundary where a safe interface meets the unsafe primitives on top of which it is built.

Consume the natural number and the proof in the Fin.

Variant of with for unboxed argument and result types.

This crashes if n = 0. Divides i by n and takes the remainder.

This crashes if n = 0. Divides i by n and takes the remainder.

Convert an Int to a finite number, testing that it is less than the upper bound. This crashes with an uncatchable exception when given a negative number.

Unboxed variant of fromInt.

Create an unlifted finite number from an unlifted natural number. The upper bound is the first type argument so that user can use type applications to clarify when it is helpful. For example:

>>> Fin.constant# @10 N4#