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
dataFractionView : 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) -> GTd0 => (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) -> GTd0 => 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
invFinSpec : (i : Finn) -> (1+finToNati) +finToNat (invFini) = n
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 = Nothing
`  It's not possible to strengthen the last element of Fin **n**.`

Totality: total
strengthenNotLastIsRight : (m : Finn) -> strengthen (invFin (FSm)) = Just (invFinm)
`  It's possible to strengthen the inverse of a succesor`

Totality: total
strengthenWeakenIsRight : (n : Finm) -> strengthen (weakenn) = Justn
`  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) -> weakenN0k~~~k
Totality: total