@@ -447,7 +447,7 @@ transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (tran
447447--------------------------------------------------------------------------------
448448
449449||| 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
451451elemBy p e [] = False
452452elemBy p e (x::xs) =
453453 if p e x then
@@ -460,7 +460,7 @@ elem : Eq a => a -> List a -> Bool
460460elem = elemBy (==)
461461
462462||| 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
464464lookupBy p e [] = Nothing
465465lookupBy p e (x::xs) =
466466 let (l, r) = x in
@@ -475,7 +475,7 @@ lookup = lookupBy (==)
475475
476476||| Check if any elements of the first list are found in the second, using
477477||| a custom comparison.
478−hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
478+hasAnyBy : %static (a -> a -> Bool) -> List a -> List a -> Bool
479479hasAnyBy p elems [] = False
480480hasAnyBy p elems (x::xs) =
481481 if elemBy p x elems then
@@ -527,7 +527,7 @@ findIndices = findIndices' Z
527527 findIndices' (S cnt) p xs
528528
529529||| 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
531531elemIndexBy p e = findIndex $ p e
532532
533533||| 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
536536elemIndex = elemIndexBy (==)
537537
538538||| 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
540540elemIndicesBy p e = findIndices $ p e
541541
542542||| 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)
572572
573573||| The nubBy function behaves just like nub, except it uses a user-supplied
574574||| 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
576576nubBy = nubBy' []
577577 where
578578 nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
@@ -595,7 +595,7 @@ nub : Eq a => List a -> List a
595595nub = nubBy (==)
596596
597597||| 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
599599deleteBy _ _ [] = []
600600deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
601601
@@ -622,7 +622,7 @@ delete = deleteBy (==)
622622(\\) = foldl (flip delete)
623623
624624||| 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
626626unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
627627
628628||| 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
747747||| @ eq the equality comparison
748748||| @ left the potential prefix
749749||| @ 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
751751isPrefixOfBy p [] right = True
752752isPrefixOfBy p left [] = False
753753isPrefixOfBy p (x::xs) (y::ys) =
@@ -760,7 +760,7 @@ isPrefixOfBy p (x::xs) (y::ys) =
760760isPrefixOf : Eq a => List a -> List a -> Bool
761761isPrefixOf = isPrefixOfBy (==)
762762
763−isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
763+isSuffixOfBy : %static (a -> a -> Bool) -> List a -> List a -> Bool
764764isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
765765
766766||| 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) =
795795||| Merge two sorted lists using an arbitrary comparison
796796||| predicate. Note that the lists must have been sorted using this
797797||| 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
799799mergeBy order [] right = right
800800mergeBy order left [] = left
801801mergeBy order (x::xs) (y::ys) =
@@ -811,7 +811,7 @@ merge = mergeBy compare
811811|||
812812||| @ cmp how to compare elements
813813||| @ 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
815815sortBy cmp [] = []
816816sortBy cmp [x] = [x]
817817sortBy cmp xs = let (x, y) = split xs in