Idris2Doc : 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.
dataHasLength : Lista -> Nat -> Type
  Ensure that the list's length is the provided natural number

Totality: total
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