Type.Set

Documentation

data Set (a :: [k])

Instances

type Insert k * a (Set k ((:) k s ss))

type Insert k * a (Set k ((:) k s ss)) = ($) [k] * (Set k) (If [k] ((==) k a s) ((:) k s ss) ((:) k s (Unwrapped * [k] (Insert k * a (Set k ss)))))

type Insert k1 * a (Set k2 ([] k2))

type Insert k1 * a (Set k2 ([] k2)) = Set k1 ((:) k1 a ([] k1))

type Index ke * a (Set k s)

type Index ke * a (Set k s) = Index ke [k] a s

type Unwrapped * [k] (Set k a)

type Unwrapped * [k] (Set k a) = a

type Concat * (Set k2 set) (Set k1 ((:) k1 s ss))

type Concat * (Set k2 set) (Set k1 ((:) k1 s ss)) = If * (In k1 [k2] s set) (Concat * (Set k2 set) (Set k1 ss)) (Concat * (Insert k1 * s (Set k2 set)) (Set k1 ss))

type Concat * (Set k1 set) (Set k2 ([] k2))

type Concat * (Set k1 set) (Set k2 ([] k2)) = Set k1 set

type family AsSet (a :: k)

Instances

type AsSet [k] lst

type AsSet [k] lst = AsSet' [k] (Reverse [k] lst)

type family AsSet' (a :: k)

Instances

type AsSet' [k] ([] k)

type AsSet' [k] ([] k) = Set (Any *) ([] (Any *))

type AsSet' [ke] ((:) ke l ls)

type AsSet' [ke] ((:) ke l ls) = Insert ke * l (AsSet' [ke] ls)

type family ToList s where ...

Equations

ToList (Set s) = s