Idris2Doc : Data.List.HasLength

Data.List.HasLength

HasLength : Lista -> Nat -> Type
Ensure that the list's length is the provided natural number
Totality: total
Constructors:
Z : HasLengthNilZ
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