on master help sign in
Added delete, union, diff to Prelude.List
commit8ba08bb8e00d73620c27e6008571b3bd7478b53b authorJohn Dobronszki <janosdobronszki@citromail.hu> dateMon 14 Apr 2014, 21:11 (13 years ago) parent9e75132
1 file changed+17
libs/prelude/Prelude/List.idr+17
libs/prelude/Prelude/List.idr+17
@@ -12,6 +12,7 @@ import Prelude.Nat
1212%access public
1313%default total
1414
15+infix 5 \\
1516infixr 7 ::,++
1617
1718%elim data List a
@@ -399,6 +400,22 @@ nubBy = nubBy' []
399400nub : Eq a => List a -> List a
400401nub = nubBy (==)
401402
403+deleteBy : (a -> a -> Bool) -> a -> List a -> List a
404+deleteBy _ _ [] = []
405+deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
406+
407+delete : (Eq a) => a -> List a -> List a
408+delete = deleteBy (==)
409+
410+(\\) : (Eq a) => List a -> List a -> List a
411+(\\) = foldl (flip delete)
412+
413+unionBy : (a -> a -> Bool) -> List a -> List a -> List a
414+unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
415+
416+union : (Eq a) => List a -> List a -> List a
417+union = unionBy (==)
418+
402419--------------------------------------------------------------------------------
403420-- Splitting and breaking lists
404421--------------------------------------------------------------------------------