@@ -47,25 +47,35 @@ isCons (x::xs) = True
4747-- Decidable Predicates
4848--------------------------------------------------------------------------------
4949
50−data NonEmpty : List a -> Type where
51− IsNonEmpty : NonEmpty (x :: xs)
50+||| Satisfiable if `xs` is non-empty (e.g., if `xs` is a cons).
51+data NonEmpty : (xs : List a) -> Type where
52+ ||| The proof that a cons cell is non-empty
53+ IsNonEmpty : NonEmpty (x :: xs)
5254
5355private
5456nonEmptyNil : NonEmpty [] -> Void
5557nonEmptyNil IsNonEmpty impossible
5658
59+||| Decide whether a list is non-empty
5760nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
5861nonEmpty [] = No nonEmptyNil
5962nonEmpty (x :: xs) = Yes IsNonEmpty
6063
61−data InBounds : Nat -> List a -> Type where
62− InFirst : InBounds Z (x :: xs)
63− InLater : InBounds k xs -> InBounds (S k) (x :: xs)
64+||| Satisfiable if `k` is a valid index into `xs`
65+|||
66+||| @ k the potential index
67+||| @ xs the list into which k may be an index
68+data InBounds : (k : Nat) -> (xs : List a) -> Type where
69+ ||| Z is a valid index into any cons cell
70+ InFirst : InBounds Z (x :: xs)
71+ ||| Valid indices can be extended
72+ InLater : InBounds k xs -> InBounds (S k) (x :: xs)
6473
6574instance Uninhabited (InBounds k []) where
6675 uninhabited InFirst impossible
6776
68−inBounds : (n : Nat) -> (xs : List a) -> Dec (InBounds n xs)
77+||| Decide whether `k` is a valid index into `xs`
78+inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
6979inBounds k [] = No uninhabited
7080inBounds Z (x :: xs) = Yes InFirst
7181inBounds (S k) (x :: xs) with (inBounds k xs)
@@ -339,7 +349,7 @@ mapMaybe f (x::xs) =
339349instance Foldable List where
340350 foldr c n [] = n
341351 foldr c n (x::xs) = c x (foldr c n xs)
342−
352+
343353 foldl f q [] = q
344354 foldl f q (x::xs) = foldl f (f q x) xs
345355
@@ -377,8 +387,13 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
377387 intersperse' sep [] = []
378388 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
379389
380−intercalate : List a -> List (List a) -> List a
381−intercalate sep l = concat $ intersperse sep l
390+||| Given a separator list and some more lists, produce a new list by
391+||| placing the separator between each of the lists.
392+|||
393+||| @ sep the separator
394+||| @ xss the lists between which the separator will be placed
395+intercalate : (sep : List a) -> (xss : List (List a)) -> List a
396+intercalate sep xss = concat $ intersperse sep xss
382397
383398||| Transposes rows and columns of a list of lists.
384399|||
@@ -483,15 +498,20 @@ findIndices = findIndices' Z
483498 else
484499 findIndices' (S cnt) p xs
485500
501+||| Find the index of the first occurrence of an element in a list, using a custom equality test.
486502elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
487503elemIndexBy p e = findIndex $ p e
488504
505+||| Find the index of the first occurrence of an element in a list,
506+||| using the default equality test for the type of list elements.
489507elemIndex : Eq a => a -> List a -> Maybe Nat
490508elemIndex = elemIndexBy (==)
491509
510+||| Find all indices for an element in a list, using a custom equality test.
492511elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
493512elemIndicesBy p e = findIndices $ p e
494513
514+||| Find all indices for an element in a list, using the default equality test for the type of list elements.
495515elemIndices : Eq a => a -> List a -> List Nat
496516elemIndices = elemIndicesBy (==)
497517
@@ -682,7 +702,12 @@ replaceOn a b l = map (\c => if c == a then b else c) l
682702-- Predicates
683703--------------------------------------------------------------------------------
684704
685−isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
705+||| Check whether a list is a prefix of another according to a user-supplied equality test.
706+|||
707+||| @ eq the equality comparison
708+||| @ left the potential prefix
709+||| @ right the list that may have `left` as its prefix
710+isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
686711isPrefixOfBy p [] right = True
687712isPrefixOfBy p left [] = False
688713isPrefixOfBy p (x::xs) (y::ys) =
@@ -777,6 +802,7 @@ listToMaybe (x::xs) = Just x
777802-- Misc
778803--------------------------------------------------------------------------------
779804
805+||| Keep the `Just` elements in a list, discarding the `Nothing` elements.
780806catMaybes : List (Maybe a) -> List a
781807catMaybes [] = []
782808catMaybes (x::xs) =
@@ -850,6 +876,7 @@ hasAnyByNilFalse p (x::xs) =
850876hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
851877hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl
852878
879+||| Implement foldl using foldr, for a later equality proof.
853880foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
854881foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
855882