Idris2Doc : Data.Fin.Extra

# Data.Fin.Extra

(*) : Fin (Sm) -> Fin (Sn) -> Fin (S (m*n))
Multiplication of `Fin`s as bounded naturals.
The resulting type has the smallest possible bound
as illustated by the relations with the `last` function.
Totality: total
Fixity Declaration: infixl operator, level 9
(+) : Finm -> Fin (Sn) -> Fin (m+n)
Addition of `Fin`s as bounded naturals.
The resulting type has the smallest possible bound
as illustated by the relations with the `last` function.
Totality: total
Fixity Declaration: infixl operator, level 8
FractionView : Nat -> Nat -> Type
A view of Nat as a quotient of some number and a finite remainder.
Totality: total
Constructor:
Fraction : (n : Nat) -> (d : Nat) -> GTdZ => (q : Nat) -> (r : Find) -> (q*d) +finToNatr = n -> FractionViewnd
congPlusLeft : (c : Fin (Sp)) -> k~~~l -> (k+c) ~~~ (l+c)
Totality: total
congPlusRight : (c : Finm) -> k~~~l -> (c+k) ~~~ (c+l)
Totality: total
divMod : (n : Nat) -> (d : Nat) -> GTdZ => FractionViewnd
Converts Nat to the fractional view with a non-zero divisor.
Totality: total
elemSmallerThanBound : (n : Finm) -> LT (finToNatn) m
A Fin's underlying natural number is smaller than the bound
Totality: total
finToNatLastIsBound : finToNatlast = n
Last's underlying natural number is the bound's predecessor
Totality: total
finToNatMultHomo : (x : Fin (Sm)) -> (y : Fin (Sn)) -> finToNat (x*y) = finToNatx*finToNaty
Totality: total
finToNatPlusHomo : (x : Finm) -> (y : Fin (Sn)) -> finToNat (x+y) = finToNatx+finToNaty
Totality: total
finToNatShift : (k : Nat) -> (a : Finn) -> finToNat (shiftka) = k+finToNata
`Shift k` shifts the underlying natural number by `k`.
Totality: total
finToNatWeakenNNeutral : (0 m : Nat) -> (k : Finn) -> finToNat (weakenNmk) = finToNatk
WeakenN does not modify the underlying natural number
Totality: total
finToNatWeakenNeutral : finToNat (weakenn) = finToNatn
Weaken does not modify the underlying natural number
Totality: total
indexOfSplitProdInverse : (f : Fin (m*n)) -> uncurryindexProd (splitProdf) = f
Totality: total
indexOfSplitSumInverse : (f : Fin (m+n)) -> indexSum (splitSumf) = f
Totality: total
indexProd : Finm -> Finn -> Fin (m*n)
Calculates the index of a square matrix of size `a * b` by indices of each side.
Totality: total
indexProdPreservesLast : (m : Nat) -> (n : Nat) -> indexProdlastlast = last
Totality: total
indexSum : Either (Finm) (Finn) -> Fin (m+n)
Converts `Fin`s that are used as indexes of parts to an index of a sum.

For example, if you have a `Vect` that is a concatenation of two `Vect`s and
you have an index either in the first or the second of the original `Vect`s,
using this function you can get an index in the concatenated one.
Totality: total
indexSumPreservesLast : (m : Nat) -> (n : Nat) -> indexSum (Rightlast) ~~~last
Totality: total
invFin : Finn -> Finn
Compute the Fin such that `k + invFin k = n - 1`
Totality: total
invFinInvolutive : (m : Finn) -> invFin (invFinm) = m
`invFin` is involutive (i.e. applied twice it is the identity)
Totality: total
invFinLastIsFZ : invFinlast = FZ
Totality: total
invFinWeakenIsFS : (m : Finn) -> invFin (weakenm) = FS (invFinm)
The inverse of a weakened element is the successor of its inverse
Totality: total
multPreservesLast : (m : Nat) -> (n : Nat) -> last*last = last
Totality: total
natToFinLTE : (n : Nat) -> (0 _ : LTnm) -> Finm
Total function to convert a nat to a Fin, given a proof
that it is less than the bound.
Totality: total
natToFinToNat : (n : Nat) -> (lte : LTnm) -> finToNat (natToFinLTEnlte) = n
Converting from a Nat to a Fin and back is the identity.
Totality: total
plusAssociative : (left : Finm) -> (centre : Fin (Sn)) -> (right : Fin (Sp)) -> (left+ (centre+right)) ~~~ ((left+centre) +right)
Totality: total
plusCommutative : (left : Fin (Sm)) -> (right : Fin (Sn)) -> (left+right) ~~~ (right+left)
Totality: total
plusPreservesLast : (m : Nat) -> (n : Nat) -> last+last = last
Totality: total
plusSuccRightSucc : (left : Finm) -> (right : Fin (Sn)) -> FS (left+right) ~~~ (left+FSright)
Totality: total
plusZeroLeftNeutral : (k : Fin (Sn)) -> (FZ+k) ~~~k
Totality: total
plusZeroRightNeutral : (k : Finm) -> (k+FZ) ~~~k
Totality: total
shiftAsPlus : (k : Fin (Sm)) -> shiftnk~~~ (last+k)
Totality: total
shiftFSLinear : (m : Nat) -> (f : Finn) -> shiftm (FSf) ~~~FS (shiftmf)
Totality: total
shiftLastIsLast : (m : Nat) -> shiftmlast~~~last
Totality: total
splitOfIndexProdInverse : (k : Finm) -> (l : Finn) -> splitProd (indexProdkl) = (k, l)
Totality: total
splitOfIndexSumInverse : (e : Either (Finm) (Finn)) -> splitSum (indexSume) = e
Totality: total
splitProd : Fin (m*n) -> (Finm, Finn)
Splits the index of a square matrix of size `a * b` to indices of each side.
Totality: total
splitSum : Fin (m+n) -> Either (Finm) (Finn)
Extracts an index of the first or the second part from the index of a sum.

For example, if you have a `Vect` that is a concatenation of the `Vect`s and
you have an index of this `Vect`, you have get an index of either left or right
original `Vect` using this function.
Totality: total
splitSumOfShift : (k : Finn) -> splitSum (shiftmk) = Rightk
Totality: total
splitSumOfWeakenN : (k : Finm) -> splitSum (weakenNnk) = Leftk
Totality: total
strengthen' : (m : Fin (Sn)) -> Either (m = last) (DPair (Finn) (\m' => finToNatm = finToNatm'))
Either tightens the bound on a Fin or proves that it's the last.
Totality: total
strengthenLastIsLeft : strengthenlast = Leftlast
It's not possible to strengthen the last element of Fin **n**.
Totality: total
strengthenNotLastIsRight : (m : Finn) -> strengthen (invFin (FSm)) = Right (invFinm)
It's possible to strengthen the inverse of a succesor
Totality: total
strengthenWeakenIsRight : (n : Finm) -> strengthen (weakenn) = Rightn
It's possible to strengthen a weakened element of Fin **m**.
Totality: total
weakenNAsPlusFZ : (k : Finn) -> weakenNmk = k+the (Fin (Sm)) FZ
Totality: total
weakenNOfPlus : (k : Finm) -> (l : Fin (Sn)) -> weakenNw (k+l) ~~~ (weakenNwk+l)
Totality: total
weakenNPlusHomo : (k : Finp) -> weakenNn (weakenNmk) ~~~weakenN (m+n) k
Totality: total
weakenNZeroIdentity : (k : Finn) -> weakenNZk~~~k
Totality: total