Idris2Doc : Data.Fin


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
FZ : Fin (Sk)
FS : Fink -> Fin (Sk)
allFins : (n : Nat) -> List1 (Fin (Sn))
All of the Fin elements
Totality: total
cast : (0 _ : m = n) -> Finm -> Finn
Cast between Fins with equal indices
Totality: total
finToInteger : Finn -> Integer
Convert a Fin to an Integer
Totality: total
finToNat : Finn -> Nat
Convert a Fin to a Nat
Totality: total
finToNatInjective : (fm : Fink) -> (fn : Fink) -> finToNatfm = finToNatfn -> fm = fn
`finToNat` is injective
Totality: total
fromInteger : (x : Integer) -> {auto 0 _ : IsJust (integerToFinxn)} -> Finn
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 : FSm = FSn -> m = n
Totality: total
integerToFin : Integer -> (n : Nat) -> Maybe (Finn)
Convert an `Integer` to a `Fin`, provided the integer is within bounds.
@n The upper bound of the Fin
Totality: total
last : Fin (Sn)
The largest element of some Fin type
Totality: total
natToFin : Nat -> (n : Nat) -> Maybe (Finn)
Totality: total
restrict : (n : Nat) -> Integer -> Fin (Sn)
Convert an Integer to a Fin in the required bounds/
This is essentially a composition of `mod` and `fromInteger`
Totality: total
shift : (m : Nat) -> Finn -> 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 (Sn) -> Either (Fin (Sn)) (Finn)
Attempt to tighten the bound on a Fin.
Return `Left` if the bound could not be tightened, or `Right` if it could.
Totality: total
weaken : Finn -> Fin (Sn)
Weaken the bound on a Fin by 1
Totality: total
weakenLTE : Finn -> LTEnm -> Finm
Weaken the bound on a Fin using a constructive comparison
Totality: total
weakenN : (0 n : Nat) -> Finm -> Fin (m+n)
Weaken the bound on a Fin by some amount
Totality: total