Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
- data Nat
- type family Elem typ typs :: Bool
- type family Index typ typs :: Nat
- type family MayIndexGo typ typs acc :: Maybe Nat
- type MayIndex typ typs = MayIndexGo typ typs Z
- type family MayFstIndexSnd ts1 ts2 :: Maybe Nat
- type family TEq t1 t2 :: Bool
- type family Length list :: Nat
- type family Append l1 l2 :: [*]
- type family AppendUniq typs typ :: [*]
- type family Union l1 l2 :: [*]
- type family UnionList' acc ls :: [*]
- type UnionList l = UnionList' [] l
- type family XReverse acc l :: [*]
- type Reverse a = XReverse [] a
- type family Delete typ typs :: [*]
- type family Replace typ1 typ2 typs :: [*]
- type TagElem tag typ typs = Replace typ (Tagged tag typ) typs
- type family And a b
- type family HSubset h1 h2
Documentation
HRemove Nat ((:) * e els) els Z | |
((~) Bool False (Elem * e els2), HRemove Nat els1 els2 i) => HRemove Nat ((:) * e els1) ((:) * e els2) (S i) | |
HUnion ([] *) ([] *) ([] *) (Nothing Nat) (Nothing Nat) | |
HUnion ([] *) ((:) * e els) ((:) * e els) (Nothing Nat) (Nothing Nat) | |
(HRemove Nat els2 elsx fi, HUnionable els1 elsx elsr, (~) Bool False (Elem * e1 elsr), (~) (Maybe Nat) (Just Nat fi) (MayFstIndexSnd * ((:) * e1 els1) els2), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * els2 ((:) * e1 els1))) => HUnion ((:) * e1 els1) els2 ((:) * e1 elsr) (Just Nat fi) (Nothing Nat) | |
HUnion ((:) * e els) ([] *) ((:) * e els) (Nothing Nat) (Nothing Nat) | |
(HUnionable els1 els2 elsr, (~) Bool False (Elem * e1 ((:) * e2 elsr)), (~) Bool False (Elem * e2 elsr), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 ((:) * e2 elsr)) (Nothing Nat) (Nothing Nat) | |
(HUnionable els1 els2 elsr, (~) Bool False (Elem * e1 elsr), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe Nat) (Just Nat si) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 elsr) (Nothing Nat) (Just Nat si) | |
(HRemove Nat els2 elsx fi, HUnionable els1 elsx elsr, (~) Bool False (Elem * e1 elsr), (~) (Maybe Nat) (Just Nat (S fi)) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe Nat) (Just Nat si) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 elsr) (Just Nat (S fi)) (Just Nat si) | |
(HUnionable els1 els2 elsr, (~) Bool False (Elem * e elsr)) => HUnion ((:) * e els1) ((:) * e els2) ((:) * e elsr) (Just Nat Z) (Just Nat Z) |
type family Elem typ typs :: Bool Source
Calculates to 'True if first type argument contained in second list element
type family Index typ typs :: Nat Source
Calculates to Nat kinded type describing the index of first argument in second argument
type family MayIndexGo typ typs acc :: Maybe Nat Source
MayIndexGo t (t : ts) acc = Just acc | |
MayIndexGo t (tt : ts) acc = MayIndexGo t ts (S acc) | |
MayIndexGo t [] acc = Nothing |
type MayIndex typ typs = MayIndexGo typ typs Z Source
type family MayFstIndexSnd ts1 ts2 :: Maybe Nat Source
MayFstIndexSnd (e : els) x = MayIndex e x | |
MayFstIndexSnd [] x = Nothing |
type family AppendUniq typs typ :: [*] Source
Append element to type list if element is not presented in list already
AppendUniq (t : ts) t = t : ts | |
AppendUniq (t : ts) t1 = t : AppendUniq ts t1 | |
AppendUniq [] t1 = `[t1]` |
type family Union l1 l2 :: [*] Source
Calculates union two lists
Union l1 [] = l1 | |
Union l1 (l : ls) = Union (AppendUniq l1 l) ls |
type family UnionList' acc ls :: [*] Source
UnionList' acc (e : es) = UnionList' (Union acc e) es | |
UnionList' acc [] = acc |
type UnionList l = UnionList' [] l Source
Union list of lists of elements. Return just unique elements of each nested list
type family Replace typ1 typ2 typs :: [*] Source
Replace first arbitrary element typ1
in type list with typ2