Idris2Doc : Data.Fin

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