data HasLength : Nat -> List a -> Type
Ensure that the list's length is the provided natural number
Totality: total
Visibility: public export
Constructors:
Z : HasLength 0 []
S : HasLength n xs -> HasLength (S n) (x :: xs)
hasLength : (xs : List a) -> HasLength (length xs) xs
This specification corresponds to the length function
Totality: total
Visibility: exporttake : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)
- Totality: total
Visibility: export hasLengthUnique : HasLength m xs -> HasLength n xs -> m = n
The length is unique
Totality: total
Visibility: exporthasLengthAppend : HasLength m xs -> HasLength n ys -> HasLength (m + n) (xs ++ ys)
- Totality: total
Visibility: export hasLengthReverse : HasLength m acc -> HasLength m (reverse acc)
- Totality: total
Visibility: export map : (f : (a -> b)) -> HasLength n xs -> HasLength n (map f xs)
- Totality: total
Visibility: export sucR : HasLength n xs -> HasLength (S n) (snoc xs x)
@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: exportdata View : (xs : List a) -> Subset Nat (flip HasLength xs) -> 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 [] (Element 0 Z)
S : (p : Subset Nat (flip HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))
view : (p : Subset Nat (flip HasLength xs)) -> View xs p
Proof that the view covers all possible cases.
Totality: total
Visibility: exportdata View : (xs : List a) -> (n : Nat) -> HasLength n xs -> 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 [] 0 Z
S : (n : Nat) -> (0 p : HasLength n xs) -> View (x :: xs) (S n) (S p)
view : (n : Nat) -> (0 p : HasLength n xs) -> View xs n p
Proof that the view covers all possible cases.
Totality: total
Visibility: export