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.

Instead of writing:
```
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.
data HasLength : List a -> Nat -> Type
  Ensure that the list's length is the provided natural number

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

Totality: total
hasLengthUnique : HasLength xs m -> HasLength xs n -> m = n
  The length is unique

Totality: total
map : (f : (a -> b)) -> HasLength xs n -> HasLength (map f xs) n
Totality: total
sucR : HasLength xs n -> HasLength (snoc xs x) (S n)
  @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