Type.Container

Documentation

type family In (el :: ke) (cont :: k) :: Bool

Instances

type In ke [k] a ([] k)

type In ke [k] a ([] k) = False

type In ke [ke] a ((:) ke l ls)

type In ke [ke] a ((:) ke l ls) = If Bool ((==) ke a l) True (In ke [ke] a ls)

type family Index2 (idx :: i) (cont :: c) :: el

Instances

type Index2 Nat [el] el n ((:) el a as)

type Index2 Nat [el] el n ((:) el a as) = If el ((==) Nat n 0) a (Index2 Nat [el] el ((-) n 1) as)

type family Index (el :: ke) (cont :: k) :: Maybe Nat

Instances

type Index ke [k] a ([] k)

type Index ke [k] a ([] k) = Nothing Nat

type Index ke * a (Set k s)

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

type Index ke * a (Recursive [k] ([] k))

type Index ke * a (Recursive [k] ([] k)) = Nothing Nat

type Index ke * a (Recursive [ke] ((:) ke l ls))

type Index ke * a (Recursive [ke] ((:) ke l ls)) = If (Maybe Nat) ((==) ke a l) (Just Nat 0) (SuccMaybe (Index ke * a (Recursive [ke] ls)))

type Index ke [ke] a ((:) ke l ls)

type Index ke [ke] a ((:) ke l ls) = If (Maybe Nat) ((==) ke a l) (Just Nat 0) (SuccMaybe (Index ke [ke] a ls))

type family IndexF (el :: ke) (cont :: k) :: Nat

Instances

type IndexF ke [ke] a ((:) ke l ls)

type IndexF ke [ke] a ((:) ke l ls) = If Nat ((==) ke a l) 0 ((+) (IndexF ke [ke] a ls) 1)

type family Append (el :: ke) (cont :: k) :: k

Instances

type Append k [k] a ([] k)

type Append k [k] a ([] k) = (:) k a ([] k)

type Append ke [a1] a2 ((:) a1 l ls)

type Append ke [a1] a2 ((:) a1 l ls) = (:) a1 l (Append ke [a1] a2 ls)

type family Insert (el :: ke) (cont :: k) :: 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 family Remove (el :: ke) (cont :: k) :: k

Instances

type Remove ke [k] a ([] k)

type Remove ke [k] a ([] k) = [] k

type Remove ke [ke] a ((:) ke l ls)

type Remove ke [ke] a ((:) ke l ls) = If [ke] ((==) ke a l) ls ((:) ke l (Remove ke [ke] a ls))

type family Empty (cont :: k) :: Bool

Instances

type Empty [k] ([] k)

type Empty [k] ([] k) = True

type Empty [a1] ((:) a1 a2 as)

type Empty [a1] ((:) a1 a2 as) = False

type family Size (cont :: k) :: Nat

Instances

type Size [k] ([] k)

type Size [k] ([] k) = 0

type Size [a1] ((:) a1 a2 as)

type Size [a1] ((:) a1 a2 as) = (+) 1 (Size [a1] as)

type family Reverse (cont :: k) :: k

Instances

type Reverse [k] lst

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

type family Unique (cont :: k) :: k

Instances

type Unique [k] lst

type Unique [k] lst = ToList k (AsSet [k] lst)

type family Diff (c :: k) (c' :: k) :: k

Instances

type Diff [k] l ([] k)

type Diff [k] l ([] k) = l

type Diff [ke] l ((:) ke e es)

type Diff [ke] l ((:) ke e es) = Diff [ke] (Remove ke [ke] e l) es

type family Union (c :: k) (c' :: k) :: k

type family Every a :: [*]

type family FromJust a where ...

Equations

FromJust (Just a) = a

type UnsafeIndex el cont = FromJust (Index el cont)