Idris2Doc : Data.List.AtIndex

# 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