Idris2Doc : Data.Fin.Properties

Data.Fin.Properties(source)

Some properties of functions defined in `Data.Fin`

Reexports

import public Data.Fin

Definitions

elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
  A Fin's underlying natural number is smaller than the bound

Totality: total
Visibility: export
finToNatLastIsBound : finToNat last = n
  Last's underlying natural number is the bound's predecessor

Totality: total
Visibility: export
finToNatWeakenNeutral : finToNat (weaken n) = finToNat n
  Weaken does not modify the underlying natural number

Totality: total
Visibility: export
finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) -> finToNat (weakenN m k) = finToNat k
  WeakenN does not modify the underlying natural number

Totality: total
Visibility: export
finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
  `Shift k` shifts the underlying natural number by `k`.

Totality: total
Visibility: export
complementSpec : (i : Fin n) -> (1 + finToNat i) + finToNat (complement i) = n
Totality: total
Visibility: export
complementWeakenIsFS : (m : Fin n) -> complement (weaken m) = FS (complement m)
  The inverse of a weakened element is the successor of its inverse

Totality: total
Visibility: export
complementLastIsFZ : complement last = FZ
Totality: total
Visibility: export
complementInvolutive : (m : Fin n) -> complement (complement m) = m
  `complement` is involutive (i.e. applied twice it is the identity)

Totality: total
Visibility: export
strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n
  It's possible to strengthen a weakened element of Fin **m**.

Totality: total
Visibility: export
strengthenLastIsLeft : strengthen last = Nothing
  It's not possible to strengthen the last element of Fin **n**.

Totality: total
Visibility: export
strengthenNotLastIsRight : (m : Fin n) -> strengthen (complement (FS m)) = Just (complement m)
  It's possible to strengthen the inverse of a successor

Totality: total
Visibility: export
strengthen' : (m : Fin (S n)) -> Either (m = last) (m' : Fin n ** finToNat m = finToNat m')
  Either tightens the bound on a Fin or proves that it's the last.

Totality: total
Visibility: export
weakenNZeroIdentity : (k : Fin n) -> weakenN 0 k ~~~ k
Totality: total
Visibility: export
shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
Totality: total
Visibility: export
shiftLastIsLast : (m : Nat) -> shift m last ~~~ last
Totality: total
Visibility: export