FWGL.Internal.TList

Documentation

type family Empty xs :: Bool

Equations

Empty `[]` = True

Empty (x : xs) = False

type Equal xs ys = And (IsSubset xs ys) (IsSubset ys xs) ~ True

type Member x xs = IsMember x xs ~ True

type family IsMember x xs :: Bool

Equations

IsMember x `[]` = False

IsMember x (x : xs) = True

IsMember y (x : xs) = IsMember y xs

class Subset xs ys

Instances

(~) Bool (IsSubset xs ys) True => Subset xs ys

type family IsSubset xs ys :: Bool

Equations

IsSubset xs xs = True

IsSubset `[]` ys = True

IsSubset (x : xs) ys = And (IsMember x ys) (IsSubset xs ys)

type family Remove x xs

Equations

Remove x `[]` = `[]`

Remove x (x : xs) = Remove x xs

Remove x (y : xs) = y : Remove x xs

type family Difference xs ys

Equations

Difference xs `[]` = xs

Difference xs (y : ys) = Difference (Remove y xs) ys

type family Append xs ys

Equations

Append `[]` ys = ys

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

type family Insert y xs

Equations

Insert y `[]` = `[y]`

Insert y (y : xs) = y : xs

Insert y (x : xs) = x : Insert y xs

type Reverse xs = Reverse' xs `[]`

type family Union xs ys

Equations

Union `[]` ys = ys

Union (x : xs) ys = Union xs (Insert x ys)

type Set xs = Union xs xs ~ xs