Idris2Doc : Data.Fin


dataFin : 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
coerce : (0 _ : m = n) -> Finm -> Finn
  Coerce 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) -> Maybe (Finn)
  Attempt to tighten the bound on a Fin.
Return the tightened bound if there is one, else nothing.

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