@@ -447,7 +447,7 @@ transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (tran
447--------------------------------------------------------------------------------
447--------------------------------------------------------------------------------
449||| Check if something is a member of a list using a custom comparison.
449||| Check if something is a member of a list using a custom comparison.
450−elemBy : (a -> a -> Bool) -> a -> List a -> Bool
450+elemBy : %static (a -> a -> Bool) -> a -> List a -> Bool
451elemBy p e [] = False
451elemBy p e [] = False
452elemBy p e (x::xs) =
452elemBy p e (x::xs) =
453 if p e x then
453 if p e x then
@@ -460,7 +460,7 @@ elem : Eq a => a -> List a -> Bool
460elem = elemBy (==)
460elem = elemBy (==)
462||| Find associated information in a list using a custom comparison.
462||| Find associated information in a list using a custom comparison.
463−lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
463+lookupBy : %static (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
464lookupBy p e [] = Nothing
464lookupBy p e [] = Nothing
465lookupBy p e (x::xs) =
465lookupBy p e (x::xs) =
466 let (l, r) = x in
466 let (l, r) = x in
@@ -475,7 +475,7 @@ lookup = lookupBy (==)
476||| Check if any elements of the first list are found in the second, using
476||| Check if any elements of the first list are found in the second, using
477||| a custom comparison.
477||| a custom comparison.
478−hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
478+hasAnyBy : %static (a -> a -> Bool) -> List a -> List a -> Bool
479hasAnyBy p elems [] = False
479hasAnyBy p elems [] = False
480hasAnyBy p elems (x::xs) =
480hasAnyBy p elems (x::xs) =
481 if elemBy p x elems then
481 if elemBy p x elems then
@@ -527,7 +527,7 @@ findIndices = findIndices' Z
527 findIndices' (S cnt) p xs
527 findIndices' (S cnt) p xs
529||| Find the index of the first occurrence of an element in a list, using a custom equality test.
529||| Find the index of the first occurrence of an element in a list, using a custom equality test.
530−elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
530+elemIndexBy : %static (a -> a -> Bool) -> a -> List a -> Maybe Nat
531elemIndexBy p e = findIndex $ p e
531elemIndexBy p e = findIndex $ p e
533||| Find the index of the first occurrence of an element in a list,
533||| Find the index of the first occurrence of an element in a list,
@@ -536,7 +536,7 @@ elemIndex : Eq a => a -> List a -> Maybe Nat
536elemIndex = elemIndexBy (==)
536elemIndex = elemIndexBy (==)
538||| Find all indices for an element in a list, using a custom equality test.
538||| Find all indices for an element in a list, using a custom equality test.
539−elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
539+elemIndicesBy : %static (a -> a -> Bool) -> a -> List a -> List Nat
540elemIndicesBy p e = findIndices $ p e
540elemIndicesBy p e = findIndices $ p e
542||| Find all indices for an element in a list, using the default equality test for the type of list elements.
542||| Find all indices for an element in a list, using the default equality test for the type of list elements.
@@ -572,7 +572,7 @@ filterSmaller {p} (x :: xs) with (p x)
573||| The nubBy function behaves just like nub, except it uses a user-supplied
573||| The nubBy function behaves just like nub, except it uses a user-supplied
574||| equality predicate instead of the overloaded == function.
574||| equality predicate instead of the overloaded == function.
575−nubBy : (a -> a -> Bool) -> List a -> List a
575+nubBy : %static (a -> a -> Bool) -> List a -> List a
576nubBy = nubBy' []
576nubBy = nubBy' []
578 nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
578 nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
@@ -595,7 +595,7 @@ nub : Eq a => List a -> List a
595nub = nubBy (==)
595nub = nubBy (==)
597||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
597||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
598−deleteBy : (a -> a -> Bool) -> a -> List a -> List a
598+deleteBy : %static (a -> a -> Bool) -> a -> List a -> List a
599deleteBy _ _ [] = []
599deleteBy _ _ [] = []
600deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
600deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
@@ -622,7 +622,7 @@ delete = deleteBy (==)
622(\\) = foldl (flip delete)
622(\\) = foldl (flip delete)
624||| The unionBy function returns the union of two lists by user-supplied equality predicate.
624||| The unionBy function returns the union of two lists by user-supplied equality predicate.
625−unionBy : (a -> a -> Bool) -> List a -> List a -> List a
625+unionBy : %static (a -> a -> Bool) -> List a -> List a -> List a
626unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
626unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
628||| Compute the union of two lists according to their `Eq` implementation.
628||| Compute the union of two lists according to their `Eq` implementation.
@@ -747,7 +747,7 @@ replaceOn a b l = map (\c => if c == a then b else c) l
747||| @ eq the equality comparison
747||| @ eq the equality comparison
748||| @ left the potential prefix
748||| @ left the potential prefix
749||| @ right the list that may have `left` as its prefix
749||| @ right the list that may have `left` as its prefix
750−isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
750+isPrefixOfBy : %static (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
751isPrefixOfBy p [] right = True
751isPrefixOfBy p [] right = True
752isPrefixOfBy p left [] = False
752isPrefixOfBy p left [] = False
753isPrefixOfBy p (x::xs) (y::ys) =
753isPrefixOfBy p (x::xs) (y::ys) =
@@ -760,7 +760,7 @@ isPrefixOfBy p (x::xs) (y::ys) =
760isPrefixOf : Eq a => List a -> List a -> Bool
760isPrefixOf : Eq a => List a -> List a -> Bool
761isPrefixOf = isPrefixOfBy (==)
761isPrefixOf = isPrefixOfBy (==)
763−isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
763+isSuffixOfBy : %static (a -> a -> Bool) -> List a -> List a -> Bool
764isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
764isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
766||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
766||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
@@ -795,7 +795,7 @@ sorted (x::xs) =
795||| Merge two sorted lists using an arbitrary comparison
795||| Merge two sorted lists using an arbitrary comparison
796||| predicate. Note that the lists must have been sorted using this
796||| predicate. Note that the lists must have been sorted using this
797||| predicate already.
797||| predicate already.
798−mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
798+mergeBy : %static (a -> a -> Ordering) -> List a -> List a -> List a
799mergeBy order [] right = right
799mergeBy order [] right = right
800mergeBy order left [] = left
800mergeBy order left [] = left
801mergeBy order (x::xs) (y::ys) =
801mergeBy order (x::xs) (y::ys) =
@@ -811,7 +811,7 @@ merge = mergeBy compare
812||| @ cmp how to compare elements
812||| @ cmp how to compare elements
813||| @ xs the list to sort
813||| @ xs the list to sort
814−sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
814+sortBy : %static (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
815sortBy cmp [] = []
815sortBy cmp [] = []
816sortBy cmp [x] = [x]
816sortBy cmp [x] = [x]
817sortBy cmp xs = let (x, y) = split xs in
817sortBy cmp xs = let (x, y) = split xs in