Documentation
type family Take (n :: Nat) (xs :: [k]) :: [k] where ... Source #
Equations
Take _1 ('[] :: [k]) = '[] :: [k] | |
Take 0 (_1 :: [k]) = '[] :: [k] | |
Take i (x ': xs :: [k]) = x ': Take (i - 1) xs | |
type family Drop (n :: Nat) (xs :: [k]) :: [k] where ... Source #
Equations
Drop _1 ('[] :: [k]) = '[] :: [k] | |
Drop 0 (xs :: [k]) = xs | |
Drop i (_1 ': xs :: [k]) = Drop (i - 1) xs | |