Data.Type.Remove

A singleton-esque type for representing the removal of an element from a type level list.

Documentation

data Remove :: [k] -> k -> [k] -> * where

Constructors

RZ :: Remove (a :< as) a as

RS :: !(Remove as a bs) -> Remove (b :< as) a (b :< bs)

Instances

Witness ØC (Without k as a bs) (Remove k as a bs)

Associated Types

type WitnessC (ØC :: Constraint) (Without k as a bs :: Constraint) (Remove k as a bs) :: Constraint

Methods

(\\) :: ØC => (Without k as a bs -> r) -> Remove k as a bs -> r

Read3 [l] l [l] (Remove l)

Methods

readsPrec3 :: Int -> ReadS (Some3 (Remove l) l k f)

Show3 [l] l [l] (Remove l)

Methods

showsPrec3 :: Int -> f a b c -> ShowS

show3 :: f a b c -> String

Ord3 [l] l [l] (Remove l)

Methods

compare3 :: f a b c -> f a b c -> Ordering

(<###) :: f a b c -> f a b c -> Bool

(>###) :: f a b c -> f a b c -> Bool

(<=###) :: f a b c -> f a b c -> Bool

(>=###) :: f a b c -> f a b c -> Bool

Eq3 [l] l [l] (Remove l)

Methods

eq3 :: f a b c -> f a b c -> Bool

neq3 :: f a b c -> f a b c -> Bool

Show2 [k] k (Remove k as)

Methods

showsPrec2 :: Int -> f a b -> ShowS

show2 :: f a b -> String

Ord2 [k] k (Remove k as)

Methods

compare2 :: f a b -> f a b -> Ordering

(<##) :: f a b -> f a b -> Bool

(>##) :: f a b -> f a b -> Bool

(<=##) :: f a b -> f a b -> Bool

(>=##) :: f a b -> f a b -> Bool

Eq2 [k] k (Remove k as)

Methods

eq2 :: f a b -> f a b -> Bool

neq2 :: f a b -> f a b -> Bool

TestEquality [k] (Remove k as a)

Methods

testEquality :: f a -> f b -> Maybe ((Remove k as a :~: a) b)

Show1 [k] (Remove k as a)

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 [k] (Remove k as a)

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Eq1 [k] (Remove k as a)

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

Without k as a bs => Known [k] (Remove k as a) bs

Associated Types

type KnownC (Remove k as a) (bs :: Remove k as a -> *) (a :: Remove k as a) :: Constraint

Methods

known :: bs a

Eq (Remove k as a bs)

Methods

(==) :: Remove k as a bs -> Remove k as a bs -> Bool

(/=) :: Remove k as a bs -> Remove k as a bs -> Bool

Ord (Remove k as a bs)

Methods

compare :: Remove k as a bs -> Remove k as a bs -> Ordering

(<) :: Remove k as a bs -> Remove k as a bs -> Bool

(<=) :: Remove k as a bs -> Remove k as a bs -> Bool

(>) :: Remove k as a bs -> Remove k as a bs -> Bool

(>=) :: Remove k as a bs -> Remove k as a bs -> Bool

max :: Remove k as a bs -> Remove k as a bs -> Remove k as a bs

min :: Remove k as a bs -> Remove k as a bs -> Remove k as a bs

Show (Remove k as a bs)

Methods

showsPrec :: Int -> Remove k as a bs -> ShowS

show :: Remove k as a bs -> String

showList :: [Remove k as a bs] -> ShowS

type WitnessC ØC (Without k as a bs) (Remove k as a bs)

type WitnessC ØC (Without k as a bs) (Remove k as a bs) = ØC

type KnownC [k] (Remove k as a) bs

type KnownC [k] (Remove k as a) bs = Without k as a bs

remLen :: Remove as a bs -> S (Len bs) :~: Len as

elimRemove :: (forall xs. p (a :< xs) a xs) -> (forall x xs ys. Remove xs a ys -> p xs a ys -> p (x :< xs) a (x :< ys)) -> Remove as a bs -> p as a bs

remIx :: Remove as a bs -> Index as a

remSub :: Length bs -> Remove as a bs -> Subset as bs

ixRem :: Index as a -> Some (Remove as a)

remProd :: Remove as a bs -> Prod f as -> (f a, Prod f bs)

remSum :: Remove as a bs -> Sum f as -> Either (f a) (Sum f bs)

class Without as a bs | as a -> bs where

Minimal complete definition

without

Methods

without :: Remove as a bs

Instances

((~) [k] cs ((:<) k b bs), Without k as a bs) => Without k ((:<) k b as) a cs

Methods

without :: Remove ((k :< b) as) a cs bs

(~) [k] as bs => Without k ((:<) k a as) a bs

Methods

without :: Remove ((k :< a) as) a bs bs

Witness ØC (Without k as a bs) (Remove k as a bs)

Associated Types

type WitnessC (ØC :: Constraint) (Without k as a bs :: Constraint) (Remove k as a bs) :: Constraint

Methods

(\\) :: ØC => (Without k as a bs -> r) -> Remove k as a bs -> r

type WitnessC ØC (Without k as a bs) (Remove k as a bs)

type WitnessC ØC (Without k as a bs) (Remove k as a bs) = ØC