Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.HSet.TypeLevel

Synopsis

Documentation

data Nat Source

Constructors

Z
S Nat

Instances

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

Equations

Elem typ [] = False
Elem typ (typ : typs) = True
Elem typ1 (typ2 : typs) = Elem typ1 typs

type family Index typ typs :: Nat Source

Calculates to Nat kinded type describing the index of first argument in second argument

Equations

Index t (t : ts) = Z
Index t (tt : ts) = S (Index t ts)

type family MayIndexGo typ typs acc :: Maybe Nat Source

Equations

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

Equations

MayFstIndexSnd (e : els) x = MayIndex e x
MayFstIndexSnd [] x = Nothing

type family TEq t1 t2 :: Bool Source

Equations

TEq a a = True
TEq a b = False

type family Length list :: Nat Source

Type level list length

Equations

Length [] = Z
Length (x : xs) = S (Length xs)

type family Append l1 l2 :: [*] Source

Equations

Append [] x = x
Append x [] = x
Append (x : xs) ys = x : Append xs ys

type family XReverse acc l :: [*] Source

Equations

XReverse acc [] = acc
XReverse acc (e : els) = XReverse (e : acc) els

type Reverse a = XReverse [] a Source

Reverse list of elements

type family Delete typ typs :: [*] Source

Delete element from type list

Equations

Delete x [] = []
Delete x (x : ys) = Delete x ys
Delete x (y : ys) = y : Delete x ys

type family And a b Source

Equations

And False x = False
And x False = False
And x y = True

type family HSubset h1 h2 Source

Checks if the former subset included in the latter one.

Equations

HSubset [] x = True
HSubset x [] = False
HSubset (h1 : tl2) h2 = And (Elem h1 h2) (HSubset tl2 h2)