Copyright	(C) 2014 Jan Stolarek
License	BSD-style (see LICENSE)
Maintainer	Jan Stolarek (jan.stolarek@p.lodz.pl)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Promotion.Prelude.Eq

Description

Provided promoted definitions related to type-level equality.

Synopsis

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

Documentation

class PEq a #

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 #

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

Instances

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

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

Instances

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

data (l :: a6989586621679303786) ==@#@$$ (l :: TyFun a6989586621679303786 Bool) #

Instances

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

type (==@#@$$$) (t :: a6989586621679303786) (t :: a6989586621679303786) = (==) t t #

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

Instances

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

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

Instances

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

type (/=@#@$$$) (t :: a6989586621679303786) (t :: a6989586621679303786) = (/=) t t #