Data.Fin

data Fin : Nat -> Type

  Numbers strictly less than some bound. The name comes from "finite sets".
  
  It's probably not a good idea to use `Fin` for arithmetic, and they will be
  exceedingly inefficient at run time.
  @ n the upper bound

Totality: total
Constructors:

FZ : Fin (S k)
FS : Fin k -> Fin (S k)

allFins : (n : Nat) -> List1 (Fin (S n))

  All of the Fin elements

Totality: total

coerce : (0 _ : m = n) -> Fin m -> Fin n

  Coerce between Fins with equal indices

Totality: total

finToInteger : Fin n -> Integer

  Convert a Fin to an Integer

Totality: total

finToNat : Fin n -> Nat

  Convert a Fin to a Nat

Totality: total

finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> finToNat fm = finToNat fn -> fm = fn

  `finToNat` is injective

Totality: total

fromInteger : (x : Integer) -> {auto 0 _ : IsJust (integerToFin x n)} -> Fin n

  Allow overloading of Integer literals for Fin.
  @ x the Integer that the user typed
  @ prf an automatically-constructed proof that `x` is in bounds

Totality: total

fsInjective : FS m = FS n -> m = n

Totality: total

integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)

  Convert an `Integer` to a `Fin`, provided the integer is within bounds.
  @n The upper bound of the Fin

Totality: total

last : Fin (S n)

  The largest element of some Fin type

Totality: total

natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

Totality: total

restrict : (n : Nat) -> Integer -> Fin (S n)

  Convert an Integer to a Fin in the required bounds/
  This is essentially a composition of `mod` and `fromInteger`

Totality: total

shift : (m : Nat) -> Fin n -> Fin (m + n)

  Add some natural number to a Fin, extending the bound accordingly
  @ n the previous bound
  @ m the number to increase the Fin by

Totality: total

strengthen : Fin (S n) -> Maybe (Fin n)

  Attempt to tighten the bound on a Fin.
  Return the tightened bound if there is one, else nothing.

Totality: total

weaken : Fin n -> Fin (S n)

  Weaken the bound on a Fin by 1

Totality: total

weakenLTE : Fin n -> LTE n m -> Fin m

  Weaken the bound on a Fin using a constructive comparison

Totality: total

weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)

  Weaken the bound on a Fin by some amount

Totality: total