Idris2Doc : Data.Fin

Data.Fin

Reexports

importpublic Control.Ord
importpublic Data.Maybe
importpublic Data.Nat
importpublic Data.So

Definitions

dataFin : 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 (Sk)
FS : Fink->Fin (Sk)

Hints:
Cast (Finn) Nat
Cast (Finn) Integer
DecEq (Finn)
Eq (Finn)
InjectiveFS
InjectivefinToNat
Neg (Fin (Sn))
Num (Fin (Sn))
Ord (Finn)
Show (Finn)
Uninhabited (Fin0)
Uninhabited (FZ=FSk)
Uninhabited (FSk=FZ)
Uninhabited (n=m) =>Uninhabited (FSn=FSm)
Uninhabited (FSk~~~FZ)
Uninhabited (FZ~~~FSk)
coerce : (0_ : m=n) ->Finm->Finn
  Coerce between Fins with equal indices

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

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

Totality: total
Visibility: public export
weaken : Finn->Fin (Sn)
  Weaken the bound on a Fin by 1

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

Totality: total
Visibility: public export
weakenLTE : Finn->LTEnm->Finm
  Weaken the bound on a Fin using a constructive comparison

Totality: total
Visibility: public export
strengthen : Fin (Sn) ->Maybe (Finn)
  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) ->Finn->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 : Finn->Finn
  Increment a Fin, wrapping on overflow

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

Totality: total
Visibility: public export
complement : Finn->Finn
  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) ->List (Finn)
  All of the Fin elements

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

Totality: total
Visibility: public export
natToFinLT : (x : Nat) -> {auto0_ : LTxn} ->Finn
Totality: total
Visibility: public export
natToFinLt : (x : Nat) -> {auto0_ : So (x<n)} ->Finn
Totality: total
Visibility: public export
natToFin : Nat-> (n : Nat) ->Maybe (Finn)
Totality: total
Visibility: public export
integerToFin : Integer-> (n : Nat) ->Maybe (Finn)
  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 (LTExy)
Totality: total
Visibility: public export
maybeLT : (x : Nat) -> (y : Nat) ->Maybe (LTxy)
Totality: total
Visibility: public export
finFromInteger : (x : Integer) -> {auto0_ : So (fromIntegerx<n)} ->Finn
Totality: total
Visibility: public export
integerLessThanNat : Integer->Nat->Bool
Totality: total
Visibility: public export
fromInteger : (x : Integer) -> {auto0_ : So (integerLessThanNatxn)} ->Finn
  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 (Sn)
  Convert an Integer to a Fin in the required bounds/
This is essentially a composition of `mod` and `fromInteger`

Totality: total
Visibility: public export
dataPointwise : Finm->Finn->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 : PointwiseFZFZ
FS : Pointwisekl->Pointwise (FSk) (FSl)
(~~~) : Finm->Finn->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 : (0eq : m=n) ->coerceeqk~~~k
  Pointwise equality is compatible with coerce

Totality: total
Visibility: export
congCoerce : k~~~l->coerceeq1k~~~coerceeq2l
  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->shiftmk~~~shiftml
Totality: total
Visibility: export
congWeakenN : k~~~l->weakenNnk~~~weakenNnl
  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 : (0eq : m=n) ->k~~~l->k=rewrite__impl{_:5275}{_:5274}l
  Pointwise equality is propositional equality modulo transport on Fins that
have provably equal types

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

Totality: total
Visibility: export
weakenNeutral : (k : Finn) ->weakenk~~~k
Totality: total
Visibility: export
weakenNNeutral : (0m : Nat) -> (k : Finn) ->weakenNmk~~~k
Totality: total
Visibility: export