Data.Fin

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

Weaken the bound on a Fin by some amount

weaken : Fin n -> Fin (S n)

Weaken the bound on a Fin by 1

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.

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

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

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

last : Fin (S n)

The largest element of some Fin type

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

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

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

finToNat is injective

finToNat : Fin n -> Nat

Convert a Fin to a Nat

finToInteger : Fin n -> Integer

Convert a Fin to an Integer

finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

FinZElim : Fin 0 -> a

FinZAbsurd : Fin 0 -> Void

There are no elements of Fin Z

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)

FZNotFS : (FZ = FS f) -> Void

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

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