Data.Fin

FSInjective : (m : Fin k) -> (n : Fin k) -> (FS m = FS n) -> m = n

FSinjective : (FS f = FS f') -> f = f'

FZNotFS : (FZ = FS f) -> Void

data Fin : (n : 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

FZ : Fin (S k)

FS : Fin k -> Fin (S k)

FinZAbsurd : Fin 0 -> Void

There are no elements of Fin Z

FinZElim : Fin 0 -> a

addFin : (x : Fin n) -> (y : Fin m) -> Fin (finToNat x + m)

Add two Fins

finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

finToInteger : Fin n -> Integer

Convert a Fin to an Integer

finToNat : Fin n -> Nat

Convert a Fin to a Nat

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

finToNat is injective

fromInteger : (x : Integer) -> {default ItIsJust prf : 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

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

last : Fin (S n)

The largest element of some Fin type

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

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

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

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

Attempt to tighten the bound on a Fin.
Return Left if the bound could not be tightened, or Right if it could.

weaken : Fin n -> Fin (S n)

Weaken the bound on a Fin by 1

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

Weaken the bound on a Fin using an inequality proof

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

Weaken the bound on a Fin by some amount