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