Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
A singleton
-esque type for representing the removal of an element from a type level list.
Documentation
data Remove :: [k] -> k -> [k] -> * where Source #
Witness ØC (Without k as a bs) (Remove k as a bs) Source # | |
Read3 [l] l [l] (Remove l) Source # | |
Show3 [l] l [l] (Remove l) Source # | |
Ord3 [l] l [l] (Remove l) Source # | |
Eq3 [l] l [l] (Remove l) Source # | |
Show2 [k] k (Remove k as) Source # | |
Ord2 [k] k (Remove k as) Source # | |
Eq2 [k] k (Remove k as) Source # | |
TestEquality [k] (Remove k as a) Source # | |
Show1 [k] (Remove k as a) Source # | |
Ord1 [k] (Remove k as a) Source # | |
Eq1 [k] (Remove k as a) Source # | |
Without k as a bs => Known [k] (Remove k as a) bs Source # | |
Eq (Remove k as a bs) Source # | |
Ord (Remove k as a bs) Source # | |
Show (Remove k as a bs) Source # | |
type WitnessC ØC (Without k as a bs) (Remove k as a bs) Source # | |
type KnownC [k] (Remove k as a) bs Source # | |
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 Source #