Idris2Doc : Data.List.AtIndex

Data.List.AtIndex

AtIndex : a -> Lista -> Nat -> Type
@AtIndex witnesses the fact that a natural number encodes a membership proof.
It is meant to be used as a runtime-irrelevant gadget to guarantee that the
natural number is indeed a valid index.
Totality: total
Constructors:
Z : AtIndexa (a::as) Z
S : AtIndexaasn -> AtIndexa (b::as) (Sn)
Member : a -> Lista -> Type
If the equality is not decidable, we may instead rely on interface resolution
Parameters: t, ts
Methods:
isMember' : SubsetNat (AtIndextts)

Implementations:
Membert (t::ts)
Membertts => Membert (u::ts)
atIndexUnique : AtIndexaasn -> AtIndexbasn -> a = b
For a given list and a given index, there is only one possible value
stored at that index in that list
Totality: total
find : DecEqa => (x : a) -> (xs : Lista) -> Dec (SubsetNat (AtIndexxxs))
Provided that equality is decidable, we can look for the first occurence
of a value inside of a list
Totality: total
inRange : (n : Nat) -> (xs : Lista) -> (0 _ : AtIndexxxsn) -> LTEn (lengthxs)
An AtIndex proof implies that n is less than the length of the list indexed into
Totality: total
inverseS : AtIndexx (y::xs) (Sn) -> AtIndexxxsn
inversion principle for S constructor
Totality: total
inverseZ : AtIndexx (y::xs) Z -> x = y
Inversion principle for Z constructor
Totality: total
isMember : (0 t : a) -> (0 ts : Lista) -> Membertts => SubsetNat (AtIndextts)
Totality: total
isMember' : Membertts => SubsetNat (AtIndextts)
Totality: total
lookup : (n : Nat) -> (xs : Lista) -> Dec (Subseta (\x => AtIndexxxsn))
Given an index, we can decide whether there is a value corresponding to it
Totality: total
strengthenL : (p : SubsetNat (HasLengthxs)) -> ltn (fstp) = True -> AtIndexx (xs++ys) n -> AtIndexxxsn
Totality: total
strengthenR : (p : SubsetNat (HasLengthws)) -> lte (fstp) n = True -> AtIndexx (ws++xs) n -> AtIndexxxs (minusn (fstp))
Totality: total
weakenL : (p : SubsetNat (HasLengthws)) -> AtIndexxxsn -> AtIndexx (ws++xs) (fstp+n)
Totality: total
weakenR : AtIndexxxsn -> AtIndexx (xs++ys) n
Totality: total