Idris2Doc : Data.Fin

# Data.Fin

## Reexports

`import public Control.Ordimport public Data.Maybeimport public Data.Natimport public Data.So`

## Definitions

`data Fin : Nat -> Type`
`  Numbers strictly less than some bound.  The name comes from "finite sets".    It's probably not a good idea to use `Fin` for arithmetic, and they will be  exceedingly inefficient at run time.  @ n the upper bound`

Totality: total
Visibility: public export
Constructors:
`FZ : Fin (S k)`
`FS : Fin k -> Fin (S k)`

Hints:
`Cast (Fin n) Nat`
`Cast (Fin n) Integer`
`DecEq (Fin n)`
`Eq (Fin n)`
`Injective FS`
`Injective finToNat`
`Neg (Fin (S n))`
`Num (Fin (S n))`
`Ord (Fin n)`
`Show (Fin n)`
`Uninhabited (Fin 0)`
`Uninhabited (FZ = FS k)`
`Uninhabited (FS k = FZ)`
`Uninhabited (n = m) => Uninhabited (FS n = FS m)`
`Uninhabited (FS k ~~~ FZ)`
`Uninhabited (FZ ~~~ FS k)`
`coerce : (0 _ : m = n) -> Fin m -> Fin n`
`  Coerce between Fins with equal indices`

Totality: total
Visibility: public export
`finToNat : Fin n -> Nat`
`  Convert a Fin to a Nat`

Totality: total
Visibility: public export
`finToInteger : Fin n -> Integer`
`  Convert a Fin to an Integer`

Totality: total
Visibility: public export
`weaken : Fin n -> Fin (S n)`
`  Weaken the bound on a Fin by 1`

Totality: total
Visibility: public export
`weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)`
`  Weaken the bound on a Fin by some amount`

Totality: total
Visibility: public export
`weakenLTE : Fin n -> LTE n m -> Fin m`
`  Weaken the bound on a Fin using a constructive comparison`

Totality: total
Visibility: public export
`strengthen : Fin (S n) -> Maybe (Fin n)`
`  Attempt to tighten the bound on a Fin.  Return the tightened bound if there is one, else nothing.`

Totality: total
Visibility: export
`shift : (m : Nat) -> Fin n -> Fin (m + n)`
`  Add some natural number to a Fin, extending the bound accordingly  @ n the previous bound  @ m the number to increase the Fin by`

Totality: total
Visibility: public export
`finS : Fin n -> Fin n`
`  Increment a Fin, wrapping on overflow`

Totality: total
Visibility: public export
`last : Fin (S n)`
`  The largest element of some Fin type`

Totality: total
Visibility: public export
`complement : Fin n -> Fin n`
`  The finite complement of some Fin.  The number as far along as the input, but starting from the other end.`

Totality: total
Visibility: public export
`allFins : (n : Nat) -> List1 (Fin (S n))`
`  All of the Fin elements`

Totality: total
Visibility: public export
`natToFinLT : (x : Nat) -> {auto 0 _ : LT x n} -> Fin n`
Totality: total
Visibility: public export
`natToFinLt : (x : Nat) -> {auto 0 _ : So (x < n)} -> Fin n`
Totality: total
Visibility: public export
`natToFin : Nat -> (n : Nat) -> Maybe (Fin n)`
Totality: total
Visibility: public export
`integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)`
`  Convert an `Integer` to a `Fin`, provided the integer is within bounds.  @n The upper bound of the Fin`

Totality: total
Visibility: public export
`maybeLTE : (x : Nat) -> (y : Nat) -> Maybe (LTE x y)`
Totality: total
Visibility: public export
`maybeLT : (x : Nat) -> (y : Nat) -> Maybe (LT x y)`
Totality: total
Visibility: public export
`finFromInteger : (x : Integer) -> {auto 0 _ : So (fromInteger x < n)} -> Fin n`
Totality: total
Visibility: public export
`integerLessThanNat : Integer -> Nat -> Bool`
Totality: total
Visibility: public export
`fromInteger : (x : Integer) -> {auto 0 _ : So (integerLessThanNat x n)} -> Fin n`
`  Allow overloading of Integer literals for Fin.  @ x the Integer that the user typed  @ prf an automatically-constructed proof that `x` is in bounds`

Totality: total
Visibility: public export
`restrict : (n : Nat) -> Integer -> Fin (S n)`
`  Convert an Integer to a Fin in the required bounds/  This is essentially a composition of `mod` and `fromInteger``

Totality: total
Visibility: public export
`data Pointwise : Fin m -> Fin n -> Type`
`  Pointwise equality of Fins  It is sometimes complicated to prove equalities on type-changing  operations on Fins.  This inductive definition can be used to simplify proof. We can  recover proofs of equalities by using `homoPointwiseIsEqual`.`

Totality: total
Visibility: public export
Constructors:
`FZ : Pointwise FZ FZ`
`FS : Pointwise k l -> Pointwise (FS k) (FS l)`
`(~~~) : Fin m -> Fin n -> Type`
`  Convenient infix notation for the notion of pointwise equality of Fins`

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6
`reflexive : k ~~~ k`
`  Pointwise equality is reflexive`

Totality: total
Visibility: export
`symmetric : k ~~~ l -> l ~~~ k`
`  Pointwise equality is symmetric`

Totality: total
Visibility: export
`transitive : j ~~~ k -> k ~~~ l -> j ~~~ l`
`  Pointwise equality is transitive`

Totality: total
Visibility: export
`coerceEq : (0 eq : m = n) -> coerce eq k ~~~ k`
`  Pointwise equality is compatible with coerce`

Totality: total
Visibility: export
`congCoerce : k ~~~ l -> coerce eq1 k ~~~ coerce eq2 l`
`  The actual proof used by coerce is irrelevant`

Totality: total
Visibility: export
`congLast : (0 _ : m = n) -> last ~~~ last`
`  Last is congruent wrt index equality`

Totality: total
Visibility: export
`congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l`
Totality: total
Visibility: export
`congWeakenN : k ~~~ l -> weakenN n k ~~~ weakenN n l`
`  WeakenN is congruent wrt pointwise equality`

Totality: total
Visibility: export
`homoPointwiseIsEqual : k ~~~ l -> k = l`
`  Pointwise equality is propositional equality on Fins that have the same type`

Totality: total
Visibility: export
`hetPointwiseIsTransport : (0 eq : m = n) -> k ~~~ l -> k = rewrite__impl {_:5314} {_:5313} l`
`  Pointwise equality is propositional equality modulo transport on Fins that  have provably equal types`

Totality: total
Visibility: export
`finToNatQuotient : k ~~~ l -> finToNat k = finToNat l`
Totality: total
Visibility: export
`finToNatEqualityAsPointwise : (k : Fin m) -> (l : Fin n) -> finToNat k = finToNat l -> k ~~~ l`
`  Propositional equality on `finToNat`s implies pointwise equality on the `Fin`s themselves`

Totality: total
Visibility: export
`weakenNeutral : (k : Fin n) -> weaken k ~~~ k`
Totality: total
Visibility: export
`weakenNNeutral : (0 m : Nat) -> (k : Fin n) -> weakenN m k ~~~ k`
Totality: total
Visibility: export