b790b61 · type-fun · git.iko.soy

src/TypeFun/Constraint.hsnew file+7

@@ -0,0 +1,7 @@

1+module TypeFun.Constraint where

2+

3+import GHC.Exts

4+

5+type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where

6+ AllSatisfy c '[] = ()

7+ AllSatisfy c (a ': as) = (c a, AllSatisfy c as)

src/TypeFun/Data/List.hs+5

@@ -89,3 +89,8 @@ type family Take (c :: N) (s :: [k]) :: [k] where

89 Take 'Z s = '[]

90 Take ('S c) '[] = '[]

91 Take ('S c) (a ': as) = a ': (Take c as)

92+

93+type family Delete (a :: k) (s :: [k]) :: [k] where

94+ Delete a '[] = '[]

95+ Delete a (a ': as) = Delete a as

96+ Delete a (b ': as) = b ': (Delete a as)

type-fun.cabal+2−1

@@ -28,7 +28,8 @@ library

28 , TypeOperators

29 , UndecidableInstances

30

31− exposed-modules: TypeFun.Data.Eq

31+ exposed-modules: TypeFun.Constraint

32+ , TypeFun.Data.Eq

32 , TypeFun.Data.List

33 , TypeFun.Data.List

33 , TypeFun.Data.Maybe

34 , TypeFun.Data.Maybe

34 , TypeFun.Data.Peano

35 , TypeFun.Data.Peano