Idris2Doc : Data.Fin.ToFin

Data.Fin.ToFin

(source)
Conversions of `Fin`s to `Fin`s

Reexports

import public Data.Fin

Definitions

tryToFit : Fin from -> Maybe (Fin to)
Totality: total
Visibility: public export
weakenOrShift : (left : Nat) -> (mid : Nat) -> Fin (left + right) -> Fin ((left + mid) + right)
Totality: total
Visibility: public export
weakenToSuper : Fin (finToNat i) -> Fin n
Totality: total
Visibility: public export
weakenToSuper_correct : (x : Fin (finToNat i)) -> finToNat (weakenToSuper x) = finToNat x
Totality: total
Visibility: export
weakenOrShiftWithNoShiftIsWeakenN : (left : Nat) -> (mid : Nat) -> (x' : Fin (left + 0)) -> (x : Fin left) -> x' ~~~ x => weakenOrShift left mid x' ~~~ weakenN mid x
Totality: total
Visibility: export