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.

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

We would write either of:
```
f1 : (n : Nat) -> (0 _ : HasLength xs n) -> P xs
f2 : (n : Subset n (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.```
dataHasLength : Lista -> Nat -> Type
`  Ensure that the list's length is the provided natural number`

Totality: total
Constructors:
Z : HasLength [] 0
S : HasLengthxsn -> HasLength (x::xs) (Sn)
hasLength : (xs : Lista) -> HasLengthxs (lengthxs)
`  This specification corresponds to the length function`

Totality: total
hasLengthUnique : HasLengthxsm -> HasLengthxsn -> m = n
`  The length is unique`

Totality: total
map : (f : (a -> b)) -> HasLengthxsn -> HasLength (mapfxs) n
Totality: total
sucR : HasLengthxsn -> HasLength (snocxsx) (Sn)
`  @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