Safe Haskell	None
Language	Haskell2010

Data.Type.Set

Contents

Synopsis

Set

Constructors

Numbered

type Singleton (t :: a) = t ':~ ('Nil :: Set a) Source #

type family Insert t (ts :: Set Type) :: Set Type where ... Source #

Equations

Insert t ('Nil :: Set Type) = t ':~ ('Nil :: Set Type)
Insert t (t ':~ ts) = t ':~ ts
Insert t (t' ':~ ts) = BOOL (InsertElse t t' ts :: (Set Type -> Type) -> () -> Type) (InsertThen t t' ts :: (Set Type -> Type) -> () -> Type) $ (Number t <=? Number t')

type family Merge (ts :: Set Type) (ts' :: Set Type) :: Set Type where ... Source #

Equations

Merge ts ('Nil :: Set Type) = ts
Merge ('Nil :: Set Type) ts' = ts'
Merge (t ':~ ts) (t ':~ ts') = t ':~ Merge ts ts'
Merge (t ':~ ts) (t' ':~ ts') = BOOL (MergeElse t ts t' ts' :: (Set Type -> Type) -> () -> Type) (MergeThen t ts t' ts' :: (Set Type -> Type) -> () -> Type) $ (Number t <=? Number t')

type (:-) t (ts :: Set Type) = Insert t ts infixr 5 Source #

type (:+:) (ts :: Set Type) (ts' :: Set Type) = Merge ts ts' infixr 5 Source #