Data.Fin.Extra

Reexports

Definitions

=DEPRECATED=

invFin : Fin n -> Fin n

Totality: total
Visibility: public export

=DEPRECATED=

invFinSpec : (i : Fin n) -> (1 + finToNat i) + finToNat (complement i) = n

Totality: total
Visibility: export

=DEPRECATED=

invFinWeakenIsFS : (m : Fin n) -> complement (weaken m) = FS (complement m)

Totality: total
Visibility: export

=DEPRECATED=

invFinLastIsFZ : complement last = FZ

Totality: total
Visibility: export

=DEPRECATED=

invFinInvolutive : (m : Fin n) -> complement (complement m) = m

Totality: total
Visibility: export

data FractionView : Nat -> Nat -> Type

  A view of Nat as a quotient of some number and a finite remainder.

Totality: total
Visibility: public export
Constructor: 

Fraction : (n : Nat) -> (d : Nat) -> GT d 0 => (q : Nat) -> (r : Fin d) -> (q * d) + finToNat r = n -> FractionView n d

divMod : (n : Nat) -> (d : Nat) -> GT d 0 => FractionView n d

  Converts Nat to the fractional view with a non-zero divisor.

Totality: total
Visibility: export

modFin : Nat -> (m : Nat) -> NonZero m => Fin m

  Compute n % m as a Fin with upper bound m.
  
  Useful, for example, when iterating through a large index, computing
  subindices as a function of the larger index (e.g. a flattened 2D-array)

Totality: total
Visibility: export

strengthenMod : Fin n -> (m : Nat) -> NonZero m => Fin m

  Tighten the bound on a Fin by taking its current bound modulo the given
  non-zero number.

Totality: total
Visibility: export

natToFinLTE : (n : Nat) -> (0 _ : LT n m) -> Fin m

  Total function to convert a nat to a Fin, given a proof
  that it is less than the bound.

Totality: total
Visibility: public export

natToFinToNat : (n : Nat) -> (lte : LT n m) -> finToNat (natToFinLTE n lte) = n

  Converting from a Nat to a Fin and back is the identity.

Totality: total
Visibility: public export