Idris2Doc : Data.List.AtIndex

Data.List.AtIndex

dataAtIndex : 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) 0
S : AtIndexaasn -> AtIndexa (b::as) (Sn)
interfaceMember : 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) 0 -> 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