Naturals bounded above by n.

Constraint synonym for naturals n s.t. Fin n is inhabited.

Construct a Fin from an Int, with bounds checks.

Generalized fin that works on any Integral type.

Like fin, but doesn't do any bounds checks. However, unlike unsafeFin, this is safe (by virtue of the type constraints).

Convert a number to a Fin, or Nothing if out of range.

finMod @n x is equivalent to fin @n (x mod (valueOf @n))

This raises an exception iff n ~ 0. It could have been written with a 0 < n constraint instead, but that would be annoying to prove repeatedly.

Decompose a number into a component modulo n and the rest.

This raises an exception iff n ~ 0. See finMod.

Convert a Fin to the underlying Int representing it.

Convert to a Fin with a larger bound.

This is equivalent to a specialization of attenuate.

Convert to a Fin with a (potentially) smaller bound.

This function throws an exception if the number is out of range of the target type.

Convert to a Fin with a (potentially) smaller bound.

Returns Nothing if the number is out of range of the target type.

shiftFin increases the value and bound of a Fin both by m.

unshiftFin decreases the value and bound of a Fin both by m.

Raises an exception if the result would be negative.

tryUnshiftFin decreases the value and bound of a Fin both by m.

Deconstructs the given Fin into one of two cases depending where it lies in the given range.

The inverse of splitFin.

embed increasing the bound by exactly one.

Shrink the bound by one if possible.

The minimal value of the given inhabited Fin type (i.e. 0).

The maximal value of the given inhabited Fin type (i.e n - 1).

Enumerate the entire domain in ascending order. This is equivalent to enumFrom 0 or enumFrom minBound, but without introducing a spurious (1 <= n) constraint.

Enumerate the entire domain in descending order. This is equivalent to reverse enumFin, but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

Equivalent to reverse (enumFromTo 0 x) but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

Equivalent to reverse (enumFromTo x maxBound) but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

Equivalent to reverse (enumFromTo y x) but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

Add, returning Nothing for out-of-range results.

Subtract, returning Nothing for out-of-range results.

Multiply, returning Nothing for out-of-range results.

Add and assert the result is in-range.

Subtract and assert the result is in-range.

Multiply and assert the result is in-range.

Add modulo n.

Raises error when intermediate results overflow Int.

Subtract modulo n.

Multiply modulo n.

Raises error when intermediate results overflow Int.

Negate modulo n.

Compared to complementFin, this is shifted by 1: complementFin 0 :: Fin n = n - 1, while modNegate 0 :: Fin n = 0.

Split a Fin of the form d*x + y into (x, y).

Reverse the order of the values of a Fin type.

(*2), but works even if 2 is out-of-bounds.

Divide by 2, rounding down.

Divide by 4, rounding down.

Given two Fins, returns one the size of the inputs' cartesian product.

The second argument is the lower-order one, i.e.

crossFin @_ @n (x+1) y = n + crossFin @_ @n x y crossFin @_ @n x (y+1) = 1 + crossFin @_ @n x y

Restricted coercion to larger Fin types.

This is also available as an Attenuable instance.

Restricted coercion to larger Fin types.

Restricted coercion to larger Fin types.

Restricted coercion to Int.

This is also available as an Attenuable instance.

Like fin, but doesn't do any bounds checks.

Decrement by 1, without the validity checks of pred.

Increment by 1, without the validity checks of succ.

Unsafe coercion between any Fin types.

Unsafe coercion to and from Int.