Data.Singletons.Prelude.Eq

Defines the SEq singleton version of the Eq type class.

Documentation

class kproxy ~ Proxy => PEq kproxy

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 (Proxy * Bool)

Associated Types

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

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

PEq Ordering (Proxy * Ordering)

Associated Types

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

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

PEq () (Proxy * ())

Associated Types

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

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

PEq [k0] (Proxy * [k0])

Associated Types

type ((Proxy * [k0]) :== (x :: Proxy * [k0])) (y :: Proxy * [k0]) :: Bool

type ((Proxy * [k0]) :/= (x :: Proxy * [k0])) (y :: Proxy * [k0]) :: Bool

PEq (Maybe k0) (Proxy * (Maybe k0))

Associated Types

type ((Proxy * (Maybe k0)) :== (x :: Proxy * (Maybe k0))) (y :: Proxy * (Maybe k0)) :: Bool

type ((Proxy * (Maybe k0)) :/= (x :: Proxy * (Maybe k0))) (y :: Proxy * (Maybe k0)) :: Bool

PEq (NonEmpty k0) (Proxy * (NonEmpty k0))

Associated Types

type ((Proxy * (NonEmpty k0)) :== (x :: Proxy * (NonEmpty k0))) (y :: Proxy * (NonEmpty k0)) :: Bool

type ((Proxy * (NonEmpty k0)) :/= (x :: Proxy * (NonEmpty k0))) (y :: Proxy * (NonEmpty k0)) :: Bool

PEq (Either k0 k1) (Proxy * (Either k0 k1))

Associated Types

type ((Proxy * (Either k0 k1)) :== (x :: Proxy * (Either k0 k1))) (y :: Proxy * (Either k0 k1)) :: Bool

type ((Proxy * (Either k0 k1)) :/= (x :: Proxy * (Either k0 k1))) (y :: Proxy * (Either k0 k1)) :: Bool

PEq (k0, k1) (Proxy * (k0, k1))

Associated Types

type ((Proxy * (k0, k1)) :== (x :: Proxy * (k0, k1))) (y :: Proxy * (k0, k1)) :: Bool

type ((Proxy * (k0, k1)) :/= (x :: Proxy * (k0, k1))) (y :: Proxy * (k0, k1)) :: Bool

PEq (k0, k1, k2) (Proxy * (k0, k1, k2))

Associated Types

type ((Proxy * (k0, k1, k2)) :== (x :: Proxy * (k0, k1, k2))) (y :: Proxy * (k0, k1, k2)) :: Bool

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

PEq (k0, k1, k2, k3) (Proxy * (k0, k1, k2, k3))

Associated Types

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

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

PEq (k0, k1, k2, k3, k4) (Proxy * (k0, k1, k2, k3, k4))

Associated Types

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

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

PEq (k0, k1, k2, k3, k4, k5) (Proxy * (k0, k1, k2, k3, k4, k5))

Associated Types

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

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

PEq (k0, k1, k2, k3, k4, k5, k6) (Proxy * (k0, k1, k2, k3, k4, k5, k6))

Associated Types

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

type ((Proxy * (k0, k1, k2, k3, k4, k5, k6)) :/= (x :: Proxy * (k0, k1, k2, k3, k4, k5, k6))) (y :: Proxy * (k0, k1, k2, k3, k4, k5, k6)) :: 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 b. Sing a -> Sing b -> Sing (a :== b) infix 4

Boolean equality on singletons

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

Boolean disequality on singletons

(%:/=) :: forall a b. (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 a0 => SEq [a0]

Methods

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

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

SEq a0 => SEq (Maybe a0)

Methods

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

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

SEq a0 => SEq (NonEmpty a0)

Methods

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

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

(SEq a0, SEq b0) => SEq (Either a0 b0)

Methods

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

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

(SEq a0, SEq b0) => SEq (a0, b0)

Methods

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

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

(SEq a0, SEq b0, SEq c0) => SEq (a0, b0, c0)

Methods

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

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

(SEq a0, SEq b0, SEq c0, SEq d0) => SEq (a0, b0, c0, d0)

Methods

(%:==) :: Sing (a0, b0, c0, d0) a -> Sing (a0, b0, c0, d0) b -> Sing Bool (((a0, b0, c0, d0) :== a) b)

(%:/=) :: Sing (a0, b0, c0, d0) a -> Sing (a0, b0, c0, d0) b -> Sing Bool (((a0, b0, c0, d0) :/= a) b)

(SEq a0, SEq b0, SEq c0, SEq d0, SEq e0) => SEq (a0, b0, c0, d0, e0)

Methods

(%:==) :: Sing (a0, b0, c0, d0, e0) a -> Sing (a0, b0, c0, d0, e0) b -> Sing Bool (((a0, b0, c0, d0, e0) :== a) b)

(%:/=) :: Sing (a0, b0, c0, d0, e0) a -> Sing (a0, b0, c0, d0, e0) b -> Sing Bool (((a0, b0, c0, d0, e0) :/= a) b)

(SEq a0, SEq b0, SEq c0, SEq d0, SEq e0, SEq f0) => SEq (a0, b0, c0, d0, e0, f0)

Methods

(%:==) :: Sing (a0, b0, c0, d0, e0, f0) a -> Sing (a0, b0, c0, d0, e0, f0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0) :== a) b)

(%:/=) :: Sing (a0, b0, c0, d0, e0, f0) a -> Sing (a0, b0, c0, d0, e0, f0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0) :/= a) b)

(SEq a0, SEq b0, SEq c0, SEq d0, SEq e0, SEq f0, SEq g0) => SEq (a0, b0, c0, d0, e0, f0, g0)

Methods

(%:==) :: Sing (a0, b0, c0, d0, e0, f0, g0) a -> Sing (a0, b0, c0, d0, e0, f0, g0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0, g0) :== a) b)

(%:/=) :: Sing (a0, b0, c0, d0, e0, f0, g0) a -> Sing (a0, b0, c0, d0, e0, f0, g0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0, g0) :/= a) b)

data (:==$) l

Instances

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

Methods

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

type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:==$) a1627662065) l0

type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:==$) a1627662065) l0 = (:==$$) a1627662065 l0

data l :==$$ l

Instances

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

Methods

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

type Apply a1627662065 Bool ((:==$$) a1627662065 l1) l0

type Apply a1627662065 Bool ((:==$$) a1627662065 l1) l0 = (:==$$$) a1627662065 l1 l0

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

data (:/=$) l

Instances

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

Methods

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

type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:/=$) a1627662065) l0

type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:/=$) a1627662065) l0 = (:/=$$) a1627662065 l0

data l :/=$$ l

Instances

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

Methods

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

type Apply a1627662065 Bool ((:/=$$) a1627662065 l1) l0

type Apply a1627662065 Bool ((:/=$$) a1627662065 l1) l0 = (:/=$$$) a1627662065 l1 l0

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