Safe Haskell | None |
---|
- data FApply = FApply
- class HReplicate2 n e l | n e -> l, l -> n where
- hReplicate2 :: Proxy n -> e -> HList l
- hReplicateApp :: (SameLength [*] [*] l as', SameLength [*] [*] as' l, HMapAux FApply as' l, HReplicate2 (HLength l) e as') => e -> HList l
- hSplitAt :: HSplitAtAux n l ([] *) a b => Proxy HNat n -> HList l -> (HList a, HList b)
- class HSplitAtAux n l a0 a b | n -> l a0 a b where
- hEnumFromTo :: Proxy a -> Proxy b -> Proxy (HEnumFromTo a b)
- type family HEnumFromTo from to :: [HNat]
- class (SameLength a b, SameLength b a) => HReverse2 a b | a -> b, b -> a where
- class HMap1 f a b where
- class HMap2 f a b where
Documentation
class HReplicate2 n e l | n e -> l, l -> n whereSource
hReplicate2 :: Proxy n -> e -> HList lSource
HReplicate2 HZero e ([] *) | |
HReplicate2 n e es' => HReplicate2 (HSucc n) e (: * e es') |
hReplicateApp :: (SameLength [*] [*] l as', SameLength [*] [*] as' l, HMapAux FApply as' l, HReplicate2 (HLength l) e as') => e -> HList lSource
hSplitAt :: HSplitAtAux n l ([] *) a b => Proxy HNat n -> HList l -> (HList a, HList b)Source
splitAt
class HSplitAtAux n l a0 a b | n -> l a0 a b whereSource
(~ [*] l b, ~ [*] a (HRevApp a0 ([] *))) => HSplitAtAux HZero l a0 a b | |
(~ [*] (: * x xs) ls, ~ [*] acc' (: * x acc), HSplitAtAux n xs acc' a b) => HSplitAtAux (HSucc n) ls acc a b |
hEnumFromTo :: Proxy a -> Proxy b -> Proxy (HEnumFromTo a b)Source
type family HEnumFromTo from to :: [HNat]Source
- n1 .. n1 + n2
class (SameLength a b, SameLength b a) => HReverse2 a b | a -> b, b -> a whereSource
(SameLength [*] [*] a b, SameLength [*] [*] b a, ~ [*] (HRevApp a ([] *)) b, ~ [*] (HRevApp b ([] *)) a) => HReverse2 a b |