Data.Type.Set

Set

data Set a

Constructors

Nil

Numbered

class Numbered a

numbered :: TypeQ -> DecsQ

Function

type Singleton t = t :~ 'Nil

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

Equations

Insert t 'Nil = t :~ 'Nil

Insert t (t :~ ts) = t :~ ts

Insert t (t' :~ ts) = BOOL (InsertElse t t' ts) (InsertThen t t' ts) $ (Number t <=? Number t')

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

Equations

Merge ts 'Nil = ts

Merge 'Nil ts' = ts'

Merge (t :~ ts) (t :~ ts') = t :~ Merge ts ts'

Merge (t :~ ts) (t' :~ ts') = BOOL (MergeElse t ts t' ts') (MergeThen t ts t' ts') $ (Number t <=? Number t')

Operator

type (:-) t ts = t `Insert` ts infixr 5

type (:+:) ts ts' = ts `Merge` ts' infixr 5