Safe Haskell	None
Language	Haskell2010

Type.Container

Documentation

type family In el cont :: Bool Source

Instances

type In k [k1] a ([] k1) = False Source
type In k [k] a ((:) k l ls) = If Bool ((==) k a l) True (In k [k] a ls) Source

type family Index2 idx cont :: el Source

Instances

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

type family Index el cont :: Maybe Nat Source

Instances

type Index k * a (Set k1 s) = Index k [k1] a s Source
type Index k * a (Recursive [k1] ([] k1)) = Nothing Nat Source
type Index k * a (Recursive [k] ((:) k l ls)) = If (Maybe Nat) ((==) k a l) (Just Nat 0) (SuccMaybe (Index k * a (Recursive [k] ls))) Source
type Index k [k1] a ([] k1) = Nothing Nat Source
type Index k [k] a ((:) k l ls) = If (Maybe Nat) ((==) k a l) (Just Nat 0) (SuccMaybe (Index k [k] a ls)) Source

type family Append el cont :: k Source

Instances

type Append [k] k a ([] k) = (:) k a ([] k) Source
type Append [k1] k a ((:) k1 l ls) = (:) k1 l (Append [k1] k a ls) Source

type family Insert el cont :: k Source

Instances

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))))) Source
type Insert * k a (Set k1 ([] k1)) = Set k ((:) k a ([] k)) Source

type family Remove el cont :: k Source

Instances

type Remove [k1] k a ([] k1) = [] k1 Source
type Remove [k] k a ((:) k l ls) = If [k] ((==) k a l) ls ((:) k l (Remove [k] k a ls)) Source

type family Empty cont :: Bool Source

Instances

type Empty [k] ([] k) = True Source
type Empty [k] ((:) k a as) = False Source

type family Size cont :: Nat Source

Instances

type Size [k] ([] k) = 0 Source
type Size [k] ((:) k a as) = (+) 1 (Size [k] as) Source

type family Reverse cont :: k Source

Instances

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

type family Unique cont :: k Source

Instances

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

type family Concat a b :: k Source

Instances

type Concat * (Set k set) (Set k1 ((:) k1 s ss)) = If * (In k1 [k] s set) (Concat * (Set k set) (Set k1 ss)) (Concat * (Insert * k1 s (Set k set)) (Set k1 ss)) Source
type Concat * (Set k set) (Set k1 ([] k1)) = Set k set Source
type Concat [k] lst ([] k) = lst Source
type Concat [k] lst ((:) k l ls) = Concat [k] (Append [k] k l lst) ls Source

type family Diff c c' :: k Source

Instances

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

type family Union c c' :: k Source

type family a <> b infixr 6 Source

Equations

a <> b = Concat a b

type family FromJust a Source

Equations