Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Eq

Description

Defines the SEq singleton version of the Eq type class.

Synopsis

class PEq a where
- type (x :: a) == (y :: a) :: Bool
- type (x :: a) /= (y :: a) :: Bool
class SEq k where
data (==@#@$) (l :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type))
data (l :: a6989586621679311772) ==@#@$$ (l :: TyFun a6989586621679311772 Bool)
type (==@#@$$$) (t :: a6989586621679311772) (t :: a6989586621679311772) = (==) t t
data (/=@#@$) (l :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type))
data (l :: a6989586621679311772) /=@#@$$ (l :: TyFun a6989586621679311772 Bool)
type (/=@#@$$$) (t :: a6989586621679311772) (t :: a6989586621679311772) = (/=) t t

Documentation

class PEq a Source #

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

Associated Types

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

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

Instances

PEq Bool Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq Type Source #
Instance details Defined in Data.Singletons.TypeRepStar Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq () Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq Void Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq [a] Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (a, b, c) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (a, b, c, d) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (a, b, c, d, e) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (a, b, c, d, e, f) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
PEq (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #

class SEq k where Source #

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 Source #

Boolean equality on singletons

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

Boolean disequality on singletons

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

Boolean disequality on singletons

Instances

SEq Bool Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SEq Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SEq Type Source #
Instance details Defined in Data.Singletons.TypeRepStar Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SEq Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SEq Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SEq () Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SEq Void Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
(SEq a, SEq [a]) => SEq [a] Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source # (%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #
SEq a => SEq (Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source # (%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #
(SEq a, SEq [a]) => SEq (NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source # (%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #
(SEq a, SEq b) => SEq (Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
(SEq a, SEq b) => SEq (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
(SEq a, SEq b, SEq c) => SEq (a, b, c) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

data (==@#@$) (l :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type)) Source #

Instances

SuppressUnusedWarnings ((==@#@$) :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source #
type Apply ((==@#@$) :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type) -> *) (l :: a6989586621679311772) Source #
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((==@#@$) :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type) -> *) (l :: a6989586621679311772) = (==@#@$$) l

data (l :: a6989586621679311772) ==@#@$$ (l :: TyFun a6989586621679311772 Bool) Source #

Instances

SuppressUnusedWarnings ((==@#@$$) :: a6989586621679311772 -> TyFun a6989586621679311772 Bool -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source #
type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 == l2

type (==@#@$$$) (t :: a6989586621679311772) (t :: a6989586621679311772) = (==) t t Source #

data (/=@#@$) (l :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type)) Source #

Instances

SuppressUnusedWarnings ((/=@#@$) :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source #
type Apply ((/=@#@$) :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type) -> *) (l :: a6989586621679311772) Source #
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((/=@#@$) :: TyFun a6989586621679311772 (TyFun a6989586621679311772 Bool -> Type) -> *) (l :: a6989586621679311772) = (/=@#@$$) l

data (l :: a6989586621679311772) /=@#@$$ (l :: TyFun a6989586621679311772 Bool) Source #

Instances

SuppressUnusedWarnings ((/=@#@$$) :: a6989586621679311772 -> TyFun a6989586621679311772 Bool -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source #
type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 /= l2

type (/=@#@$$$) (t :: a6989586621679311772) (t :: a6989586621679311772) = (/=) t t Source #