Noether.Lemmata.TypeFu.Set

Documentation

type TSet s = Nub (Sort s)

type TSet' s = Sort s

type family Cmp (a :: k) (b :: k) :: Ordering

Instances

type Cmp Symbol k k'

type Cmp Symbol k k' = CmpSymbol k k'

type Cmp * (Tagged s1 _1 _3) (Tagged s2 _ _2)

type Cmp * (Tagged s1 _1 _3) (Tagged s2 _ _2) = Cmp Symbol s1 s2

type Cmp * ((:=) k1 Symbol k _1) ((:=) k2 Symbol k' _)

type Cmp * ((:=) k1 Symbol k _1) ((:=) k2 Symbol k' _) = CmpSymbol k k'

type family (x :: [k]) ++ (y :: [k]) :: [k] where ...

Equations

'[] ++ xs = xs

(x ': xs) ++ ys = x ': (xs ++ ys)

type family (a :: Bool) ^^ (b :: Bool) :: Bool where ...

Equations

x ^^ x = False

_ ^^ _ = True

type family Nub t where ...

Equations

Nub '[] = '[]

Nub '[e] = '[e]

Nub (e ': (e ': s)) = Nub (e ': s)

Nub (e ': (f ': s)) = e ': Nub (f ': s)

type family Sort (xs :: [k]) :: [k] where ...

Equations

Sort '[] = '[]

Sort (x ': xs) = (Sort (Filter False x xs) ++ '[x]) ++ Sort (Filter True x xs)

type family Filter (f :: Bool) (p :: k) (xs :: [k]) :: [k] where ...

Equations

Filter _ _ '[] = '[]

Filter f p (x ': xs) = IfCons (f ^^ (Cmp x p == LT)) x (Filter f p xs)

type family IfCons (pred :: Bool) (x :: k) (xs :: [k]) :: [k] where ...

Equations

IfCons False _ xs = xs

IfCons True x xs = x ': xs