typelevel-1.2.3: Useful type level operations (type families and related operators).

Safe HaskellNone
LanguageHaskell2010

Type.Container

Documentation

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

Instances
type In (a :: ke) ([] :: [k]) Source # 
Instance details

Defined in Type.List

type In (a :: ke) ([] :: [k]) = False
type In (a :: ke) (l ': ls :: [ke]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Index2 (n :: Nat) (a ': as :: [el]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Index (a :: ke) ([] :: [k]) Source # 
Instance details

Defined in Type.List

type Index (a :: ke) ([] :: [k]) = (Nothing :: Maybe Nat)
type Index (a :: ke) (Set s :: Type) Source # 
Instance details

Defined in Type.Set

type Index (a :: ke) (Set s :: Type) = Index a s
type Index (a :: ke) (Recursive ([] :: [k]) :: Type) Source # 
Instance details

Defined in Type.List

type Index (a :: ke) (Recursive ([] :: [k]) :: Type) = (Nothing :: Maybe Nat)
type Index (a :: ke) (Recursive (l ': ls) :: Type) Source # 
Instance details

Defined in Type.List

type Index (a :: ke) (Recursive (l ': ls) :: Type) = If (a == l) (Just 0) (SuccMaybe (Index a (Recursive ls)))
type Index (a :: ke) (l ': ls :: [ke]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type IndexF (a :: ke) (l ': ls :: [ke]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Append (a :: k) ([] :: [k]) Source # 
Instance details

Defined in Type.List

type Append (a :: k) ([] :: [k]) = a ': ([] :: [k])
type Append (a2 :: ke) (l ': ls :: [a1]) Source # 
Instance details

Defined in Type.List

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

type family Insert (el :: ke) (cont :: k) :: k Source #

Instances
type Insert (a :: k) (Set (s ': ss) :: Type) Source # 
Instance details

Defined in Type.Set

type Insert (a :: k) (Set (s ': ss) :: Type) = (Set :: [k] -> Type) $ If (a == s) (s ': ss) (s ': (Unwrapped (Insert a (Set ss)) :: [k]))
type Insert (a :: k1) (Set ([] :: [k2]) :: Type) Source # 
Instance details

Defined in Type.Set

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

type family Remove (el :: ke) (cont :: k) :: k Source #

Instances
type Remove (a :: ke) ([] :: [k]) Source # 
Instance details

Defined in Type.List

type Remove (a :: ke) ([] :: [k]) = ([] :: [k])
type Remove (a :: ke) (l ': ls :: [ke]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Empty ([] :: [k]) Source # 
Instance details

Defined in Type.List

type Empty ([] :: [k]) = True
type Empty (a2 ': as :: [a1]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Size ([] :: [k]) Source # 
Instance details

Defined in Type.List

type Size ([] :: [k]) = 0
type Size (a2 ': as :: [a1]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Reverse (lst :: [k]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Unique (lst :: [k]) Source # 
Instance details

Defined in Type.List

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

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

Instances
type Diff (l :: [k]) ([] :: [k]) Source # 
Instance details

Defined in Type.List

type Diff (l :: [k]) ([] :: [k]) = l
type Diff (l :: [ke]) (e ': es :: [ke]) Source # 
Instance details

Defined in Type.List

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

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

type family Every a :: [*] Source #

type family FromJust a where ... Source #

Equations

FromJust (Just a) = a 

type UnsafeIndex el cont = FromJust (Index el cont) Source #