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:
```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

dataHasLength : Nat->Lista->Type
  Ensure that the list's length is the provided natural number

Totality: total
Visibility: public export
Constructors:
Z : HasLength0 []
S : HasLengthnxs->HasLength (Sn) (x::xs)
hasLength : (xs : Lista) ->HasLength (lengthxs) xs
  This specification corresponds to the length function

Totality: total
Visibility: export
take : (n : Nat) -> (xs : Streama) ->HasLengthn (takenxs)
Totality: total
Visibility: export
hasLengthUnique : HasLengthmxs->HasLengthnxs->m=n
  The length is unique

Totality: total
Visibility: export
hasLengthAppend : HasLengthmxs->HasLengthnys->HasLength (m+n) (xs++ys)
Totality: total
Visibility: export
hasLengthReverse : HasLengthmacc->HasLengthm (reverseacc)
Totality: total
Visibility: export
map : (f : (a->b)) ->HasLengthnxs->HasLengthn (mapfxs)
Totality: total
Visibility: export
sucR : HasLengthnxs->HasLength (Sn) (snocxsx)
  @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
dataView : (xs : Lista) ->SubsetNat (flipHasLengthxs) ->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 [] (Element0Z)
S : (p : SubsetNat (flipHasLengthxs)) ->View (x::xs) (Element (S (fstp)) (S (sndp)))
view : (p : SubsetNat (flipHasLengthxs)) ->Viewxsp
  Proof that the view covers all possible cases.

Totality: total
Visibility: export
dataView : (xs : Lista) -> (n : Nat) ->HasLengthnxs->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 [] 0Z
S : (n : Nat) -> (0p : HasLengthnxs) ->View (x::xs) (Sn) (Sp)
view : (n : Nat) -> (0p : HasLengthnxs) ->Viewxsnp
  Proof that the view covers all possible cases.

Totality: total
Visibility: export