Data.Fin.Split

Splitting operations and their properties

Reexports

import public Data.Fin

Definitions

indexSum : Either (Fin m) (Fin n) -> 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
Visibility: public export

splitSum : Fin (m + n) -> Either (Fin m) (Fin n)

  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
Visibility: public export

indexProd : Fin m -> Fin n -> Fin (m * n)

  Calculates the index of a square matrix of size `a * b` by indices of each side.

Totality: total
Visibility: public export

splitProd : Fin (m * n) -> (Fin m, Fin n)

  Splits the index of a square matrix of size `a * b` to indices of each side.

Totality: total
Visibility: public export

indexSumPreservesLast : (m : Nat) -> (n : Nat) -> indexSum (Right last) ~~~ last