- 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