Data.List.AtIndex

Definitions

data AtIndex : a -> List a -> 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
Visibility: public export
Constructors:

Z : AtIndex a (a :: as) 0

S : AtIndex a as n -> AtIndex a (b :: as) (S n)

Hint: 

Uninhabited (AtIndex a [] n)

inverseZ : AtIndex x (y :: xs) 0 -> x = y

  Inversion principle for Z constructor

Totality: total
Visibility: export

inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n

  inversion principle for S constructor

Totality: total
Visibility: export

atIndexUnique : AtIndex a as n -> AtIndex b as n -> 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
Visibility: export

find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs))

  Provided that equality is decidable, we can look for the first occurence
  of a value inside of a list

Totality: total
Visibility: public export

interface Member : a -> List a -> Type

  If the equality is not decidable, we may instead rely on interface resolution

Parameters: t, ts
Methods:

isMember' : Subset Nat (AtIndex t ts)

Implementations:

Member t (t :: ts)

Member t ts => Member t (u :: ts)

isMember' : Member t ts => Subset Nat (AtIndex t ts)

Totality: total
Visibility: public export

isMember : (0 t : a) -> (0 ts : List a) -> Member t ts => Subset Nat (AtIndex t ts)

Totality: total
Visibility: public export

lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\x => AtIndex x xs n))

  Given an index, we can decide whether there is a value corresponding to it

Totality: total
Visibility: public export

inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs)

  An AtIndex proof implies that n is less than the length of the list indexed into

Totality: total
Visibility: public export

weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n

Totality: total
Visibility: export

weakenL : (p : Subset Nat (flip HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)

Totality: total
Visibility: export

strengthenL : (p : Subset Nat (flip HasLength xs)) -> lt n (fst p) = True -> AtIndex x (xs ++ ys) n -> AtIndex x xs n

Totality: total
Visibility: export

strengthenR : (p : Subset Nat (flip HasLength ws)) -> lte (fst p) n = True -> AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))

Totality: total
Visibility: export