Idris2Doc : Data.List.HasLength

# Data.List.HasLength

```This module implements a relation between a natural number and a list.
The relation witnesses the fact the number is the length of the list.

It is meant to be used in a runtime-irrelevant fashion in computations
manipulating data indexed over lists where the computation actually only
depends on the length of said lists.

```idris example
f0 : (xs : List a) -> P xs
```

We would write either of:
```idris example
f1 : (n : Nat) -> (0 _ : HasLength n xs) -> P xs
f2 : (n : Subset n (flip HasLength xs)) -> P xs
```

See `sucR` for an example where the update to the runtime-relevant Nat is O(1)
but the udpate to the list (were we to keep it around) an O(n) traversal.
```

## Definitions

`data HasLength : Nat -> List a -> Type`
`  Ensure that the list's length is the provided natural number`

Totality: total
Visibility: public export
Constructors:
`Z : HasLength 0 []`
`S : HasLength n xs -> HasLength (S n) (x :: xs)`
`hasLength : (xs : List a) -> HasLength (length xs) xs`
`  This specification corresponds to the length function`

Totality: total
Visibility: export
`take : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)`
Totality: total
Visibility: export
`hasLengthUnique : HasLength m xs -> HasLength n xs -> m = n`
`  The length is unique`

Totality: total
Visibility: export
`hasLengthAppend : HasLength m xs -> HasLength n ys -> HasLength (m + n) (xs ++ ys)`
Totality: total
Visibility: export
`hasLengthReverse : HasLength m acc -> HasLength m (reverse acc)`
Totality: total
Visibility: export
`map : (f : (a -> b)) -> HasLength n xs -> HasLength n (map f xs)`
Totality: total
Visibility: export
`sucR : HasLength n xs -> HasLength (S n) (snoc xs x)`
`  @sucR demonstrates that snoc only increases the lenght by one  So performing this operation while carrying the list around would cost O(n)  but relying on n together with an erased HasLength proof instead is O(1)`

Totality: total
Visibility: export
`data View : (xs : List a) -> Subset Nat (flip HasLength xs) -> Type`
`  We provide this view as a convenient way to perform nested pattern-matching  on values of type `Subset Nat (flip HasLength xs)`. Functions using this view will  be seen as terminating as long as the index list `xs` is left untouched.  See e.g. listTerminating below for such a function.`

Totality: total
Visibility: public export
Constructors:
`Z : View [] (Element 0 Z)`
`S : (p : Subset Nat (flip HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))`
`view : (p : Subset Nat (flip HasLength xs)) -> View xs p`
`  Proof that the view covers all possible cases.`

Totality: total
Visibility: export
`data View : (xs : List a) -> (n : Nat) -> HasLength n xs -> Type`
`  We provide this view as a convenient way to perform nested pattern-matching  on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations  to the list between recursive calls (e.g. mapping over the list) that prevent  it from being a valid termination metric, it is best to take the Nat argument  separately from the HasLength proof and the Subset view is not as useful anymore.  See e.g. natTerminating below for (a contrived example of) such a function.`

Totality: total
Visibility: public export
Constructors:
`Z : View [] 0 Z`
`S : (n : Nat) -> (0 p : HasLength n xs) -> View (x :: xs) (S n) (S p)`
`view : (n : Nat) -> (0 p : HasLength n xs) -> View xs n p`
`  Proof that the view covers all possible cases.`

Totality: total
Visibility: export