IdrisDoc: Data.Fin

# 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

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 :
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