Data.Singletons.Prelude.Eq

Defines the SEq singleton version of the Eq type class.

Documentation

class PEq a

The promoted analogue of Eq. If you supply no definition for '(:==)', then it defaults to a use of '(==)', from Data.Type.Equality.

Associated Types

type (x :: a) :== (y :: a) :: Bool infix 4

type (x :: a) :/= (y :: a) :: Bool infix 4

Instances

PEq Bool

Associated Types

type (Bool :== (x :: Bool)) (y :: Bool) :: Bool

type (Bool :/= (x :: Bool)) (y :: Bool) :: Bool

PEq Ordering

Associated Types

type (Ordering :== (x :: Ordering)) (y :: Ordering) :: Bool

type (Ordering :/= (x :: Ordering)) (y :: Ordering) :: Bool

PEq ()

Associated Types

type (() :== (x :: ())) (y :: ()) :: Bool

type (() :/= (x :: ())) (y :: ()) :: Bool

PEq [k]

Associated Types

type ([k] :== (x :: [k])) (y :: [k]) :: Bool

type ([k] :/= (x :: [k])) (y :: [k]) :: Bool

PEq (Maybe k)

Associated Types

type ((Maybe k) :== (x :: Maybe k)) (y :: Maybe k) :: Bool

type ((Maybe k) :/= (x :: Maybe k)) (y :: Maybe k) :: Bool

PEq (NonEmpty k)

Associated Types

type ((NonEmpty k) :== (x :: NonEmpty k)) (y :: NonEmpty k) :: Bool

type ((NonEmpty k) :/= (x :: NonEmpty k)) (y :: NonEmpty k) :: Bool

PEq (Either k1 k2)

Associated Types

type ((Either k1 k2) :== (x :: Either k1 k2)) (y :: Either k1 k2) :: Bool

type ((Either k1 k2) :/= (x :: Either k1 k2)) (y :: Either k1 k2) :: Bool

PEq (k1, k2)

Associated Types

type ((k1, k2) :== (x :: (k1, k2))) (y :: (k1, k2)) :: Bool

type ((k1, k2) :/= (x :: (k1, k2))) (y :: (k1, k2)) :: Bool

PEq (k1, k2, k3)

Associated Types

type ((k1, k2, k3) :== (x :: (k1, k2, k3))) (y :: (k1, k2, k3)) :: Bool

type ((k1, k2, k3) :/= (x :: (k1, k2, k3))) (y :: (k1, k2, k3)) :: Bool

PEq (k1, k2, k3, k4)

Associated Types

type ((k1, k2, k3, k4) :== (x :: (k1, k2, k3, k4))) (y :: (k1, k2, k3, k4)) :: Bool

type ((k1, k2, k3, k4) :/= (x :: (k1, k2, k3, k4))) (y :: (k1, k2, k3, k4)) :: Bool

PEq (k1, k2, k3, k4, k5)

Associated Types

type ((k1, k2, k3, k4, k5) :== (x :: (k1, k2, k3, k4, k5))) (y :: (k1, k2, k3, k4, k5)) :: Bool

type ((k1, k2, k3, k4, k5) :/= (x :: (k1, k2, k3, k4, k5))) (y :: (k1, k2, k3, k4, k5)) :: Bool

PEq (k1, k2, k3, k4, k5, k6)

Associated Types

type ((k1, k2, k3, k4, k5, k6) :== (x :: (k1, k2, k3, k4, k5, k6))) (y :: (k1, k2, k3, k4, k5, k6)) :: Bool

type ((k1, k2, k3, k4, k5, k6) :/= (x :: (k1, k2, k3, k4, k5, k6))) (y :: (k1, k2, k3, k4, k5, k6)) :: Bool

PEq (k1, k2, k3, k4, k5, k6, k7)

Associated Types

type ((k1, k2, k3, k4, k5, k6, k7) :== (x :: (k1, k2, k3, k4, k5, k6, k7))) (y :: (k1, k2, k3, k4, k5, k6, k7)) :: Bool

type ((k1, k2, k3, k4, k5, k6, k7) :/= (x :: (k1, k2, k3, k4, k5, k6, k7))) (y :: (k1, k2, k3, k4, k5, k6, k7)) :: Bool

class SEq k where

The singleton analogue of Eq. Unlike the definition for Eq, it is required that instances define a body for '(%:==)'. You may also supply a body for '(%:/=)'.

Minimal complete definition

(%:==)

Methods

(%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :== b) infix 4

Boolean equality on singletons

(%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/= b) infix 4

Boolean disequality on singletons

(%:/=) :: forall (a :: k) (b :: k). (a :/= b) ~ Not (a :== b) => Sing a -> Sing b -> Sing (a :/= b) infix 4

Boolean disequality on singletons

Instances

SEq Bool

Methods

(%:==) :: Sing Bool a -> Sing Bool b -> Sing Bool ((Bool :== a) b)

(%:/=) :: Sing Bool a -> Sing Bool b -> Sing Bool ((Bool :/= a) b)

SEq Ordering

Methods

(%:==) :: Sing Ordering a -> Sing Ordering b -> Sing Bool ((Ordering :== a) b)

(%:/=) :: Sing Ordering a -> Sing Ordering b -> Sing Bool ((Ordering :/= a) b)

SEq ()

Methods

(%:==) :: Sing () a -> Sing () b -> Sing Bool ((() :== a) b)

(%:/=) :: Sing () a -> Sing () b -> Sing Bool ((() :/= a) b)

SEq a => SEq [a]

Methods

(%:==) :: Sing [a] a -> Sing [a] b -> Sing Bool (([a] :== a) b)

(%:/=) :: Sing [a] a -> Sing [a] b -> Sing Bool (([a] :/= a) b)

SEq a => SEq (Maybe a)

Methods

(%:==) :: Sing (Maybe a) a -> Sing (Maybe a) b -> Sing Bool ((Maybe a :== a) b)

(%:/=) :: Sing (Maybe a) a -> Sing (Maybe a) b -> Sing Bool ((Maybe a :/= a) b)

SEq a => SEq (NonEmpty a)

Methods

(%:==) :: Sing (NonEmpty a) a -> Sing (NonEmpty a) b -> Sing Bool ((NonEmpty a :== a) b)

(%:/=) :: Sing (NonEmpty a) a -> Sing (NonEmpty a) b -> Sing Bool ((NonEmpty a :/= a) b)

(SEq a, SEq b) => SEq (Either a b)

Methods

(%:==) :: Sing (Either a b) a -> Sing (Either a b) b -> Sing Bool ((Either a b :== a) b)

(%:/=) :: Sing (Either a b) a -> Sing (Either a b) b -> Sing Bool ((Either a b :/= a) b)

(SEq a, SEq b) => SEq (a, b)

Methods

(%:==) :: Sing (a, b) a -> Sing (a, b) b -> Sing Bool (((a, b) :== a) b)

(%:/=) :: Sing (a, b) a -> Sing (a, b) b -> Sing Bool (((a, b) :/= a) b)

(SEq a, SEq b, SEq c) => SEq (a, b, c)

Methods

(%:==) :: Sing (a, b, c) a -> Sing (a, b, c) b -> Sing Bool (((a, b, c) :== a) b)

(%:/=) :: Sing (a, b, c) a -> Sing (a, b, c) b -> Sing Bool (((a, b, c) :/= a) b)

(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d)

Methods

(%:==) :: Sing (a, b, c, d) a -> Sing (a, b, c, d) b -> Sing Bool (((a, b, c, d) :== a) b)

(%:/=) :: Sing (a, b, c, d) a -> Sing (a, b, c, d) b -> Sing Bool (((a, b, c, d) :/= a) b)

(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e)

Methods

(%:==) :: Sing (a, b, c, d, e) a -> Sing (a, b, c, d, e) b -> Sing Bool (((a, b, c, d, e) :== a) b)

(%:/=) :: Sing (a, b, c, d, e) a -> Sing (a, b, c, d, e) b -> Sing Bool (((a, b, c, d, e) :/= a) b)

(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f)

Methods

(%:==) :: Sing (a, b, c, d, e, f) a -> Sing (a, b, c, d, e, f) b -> Sing Bool (((a, b, c, d, e, f) :== a) b)

(%:/=) :: Sing (a, b, c, d, e, f) a -> Sing (a, b, c, d, e, f) b -> Sing Bool (((a, b, c, d, e, f) :/= a) b)

(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g)

Methods

(%:==) :: Sing (a, b, c, d, e, f, g) a -> Sing (a, b, c, d, e, f, g) b -> Sing Bool (((a, b, c, d, e, f, g) :== a) b)

(%:/=) :: Sing (a, b, c, d, e, f, g) a -> Sing (a, b, c, d, e, f, g) b -> Sing Bool (((a, b, c, d, e, f, g) :/= a) b)

data (:==$) (l :: TyFun a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type))

Instances

SuppressUnusedWarnings (TyFun a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type) -> *) ((:==$) a6989586621679297822)

Methods

suppressUnusedWarnings :: Proxy ((:==$) a6989586621679297822) t -> ()

type Apply a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type) ((:==$) a6989586621679297822) l

type Apply a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type) ((:==$) a6989586621679297822) l = (:==$$) a6989586621679297822 l

data (l :: a6989586621679297822) :==$$ (l :: TyFun a6989586621679297822 Bool)

Instances

SuppressUnusedWarnings (a6989586621679297822 -> TyFun a6989586621679297822 Bool -> *) ((:==$$) a6989586621679297822)

Methods

suppressUnusedWarnings :: Proxy ((:==$$) a6989586621679297822) t -> ()

type Apply a Bool ((:==$$) a l1) l2

type Apply a Bool ((:==$$) a l1) l2 = (:==) a l1 l2

type (:==$$$) (t :: a6989586621679297822) (t :: a6989586621679297822) = (:==) t t

data (:/=$) (l :: TyFun a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type))

Instances

SuppressUnusedWarnings (TyFun a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type) -> *) ((:/=$) a6989586621679297822)

Methods

suppressUnusedWarnings :: Proxy ((:/=$) a6989586621679297822) t -> ()

type Apply a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type) ((:/=$) a6989586621679297822) l

type Apply a6989586621679297822 (TyFun a6989586621679297822 Bool -> Type) ((:/=$) a6989586621679297822) l = (:/=$$) a6989586621679297822 l

data (l :: a6989586621679297822) :/=$$ (l :: TyFun a6989586621679297822 Bool)

Instances

SuppressUnusedWarnings (a6989586621679297822 -> TyFun a6989586621679297822 Bool -> *) ((:/=$$) a6989586621679297822)

Methods

suppressUnusedWarnings :: Proxy ((:/=$$) a6989586621679297822) t -> ()

type Apply a Bool ((:/=$$) a l1) l2

type Apply a Bool ((:/=$$) a l1) l2 = (:/=) a l1 l2

type (:/=$$$) (t :: a6989586621679297822) (t :: a6989586621679297822) = (:/=) t t