Data.Fin.Arith

Result-type changing `Fin` arithmetics

Reexports

Definitions

(+) : Fin m -> Fin (S n) -> Fin (m + n)

  Addition of `Fin`s as bounded naturals.
  The resulting type has the smallest possible bound
  as illustrated by the relations with the `last` function.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

(*) : Fin (S m) -> Fin (S n) -> 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
Visibility: public export
Fixity Declaration: infixl operator, level 9

finToNatPlusHomo : (x : Fin m) -> (y : Fin (S n)) -> finToNat (x + y) = finToNat x + finToNat y

Totality: total
Visibility: export

finToNatMultHomo : (x : Fin (S m)) -> (y : Fin (S n)) -> finToNat (x * y) = finToNat x * finToNat y

Totality: total
Visibility: export

plusPreservesLast : (m : Nat) -> (n : Nat) -> last + last = last

Totality: total
Visibility: export

multPreservesLast : (m : Nat) -> (n : Nat) -> last * last = last

Totality: total
Visibility: export

plusSuccRightSucc : (left : Fin m) -> (right : Fin (S n)) -> FS (left + right) ~~~ (left + FS right)

Totality: total
Visibility: export

shiftAsPlus : (k : Fin (S m)) -> shift n k ~~~ (last + k)

Totality: total
Visibility: export

weakenNAsPlusFZ : (k : Fin n) -> weakenN m k = k + the (Fin (S m)) FZ

Totality: total
Visibility: export

weakenNPlusHomo : (k : Fin p) -> weakenN n (weakenN m k) ~~~ weakenN (m + n) k

Totality: total
Visibility: export

weakenNOfPlus : (k : Fin m) -> (l : Fin (S n)) -> weakenN w (k + l) ~~~ (weakenN w k + l)

Totality: total
Visibility: export

plusZeroLeftNeutral : (k : Fin (S n)) -> (FZ + k) ~~~ k

Totality: total
Visibility: export

congPlusLeft : (c : Fin (S p)) -> k ~~~ l -> (k + c) ~~~ (l + c)

Totality: total
Visibility: export

plusZeroRightNeutral : (k : Fin m) -> (k + FZ) ~~~ k

Totality: total
Visibility: export

congPlusRight : (c : Fin m) -> k ~~~ l -> (c + k) ~~~ (c + l)

Totality: total
Visibility: export

plusCommutative : (left : Fin (S m)) -> (right : Fin (S n)) -> (left + right) ~~~ (right + left)

Totality: total
Visibility: export

plusAssociative : (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) -> (left + (centre + right)) ~~~ ((left + centre) + right)

Totality: total
Visibility: export