| 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
- class SEq k where
- data (==@#@$) (l :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type))
- data (l :: a6989586621679304361) ==@#@$$ (l :: TyFun a6989586621679304361 Bool)
- type (==@#@$$$) (t :: a6989586621679304361) (t :: a6989586621679304361) = (==) t t
- data (/=@#@$) (l :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type))
- data (l :: a6989586621679304361) /=@#@$$ (l :: TyFun a6989586621679304361 Bool)
- type (/=@#@$$$) (t :: a6989586621679304361) (t :: a6989586621679304361) = (/=) t t
Documentation
The promoted analogue of Eq. If you supply no definition for '(==)',
then it defaults to a use of '(DTE.==)', from Data.Type.Equality.
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 # | |
| SEq Ordering # | |
| SEq Type # | |
| SEq Nat # | |
| SEq Symbol # | |
| SEq () # | |
| SEq Void # | |
| (SEq a, SEq [a]) => SEq [a] # | |
| SEq a => SEq (Maybe a) # | |
| (SEq a, SEq [a]) => SEq (NonEmpty a) # | |
| (SEq a, SEq b) => SEq (Either a b) # | |
| (SEq a, SEq b) => SEq (a, b) # | |
| (SEq a, SEq b, SEq c) => SEq (a, b, c) # | |
| (SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) # | |
| (SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) # | |
| (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) # | |
| (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) # | |
data (==@#@$) (l :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type)) #
Instances
| SuppressUnusedWarnings ((==@#@$) :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type) -> *) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((==@#@$) :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type) -> *) (l :: a6989586621679304361) # | |
data (l :: a6989586621679304361) ==@#@$$ (l :: TyFun a6989586621679304361 Bool) #
Instances
| SuppressUnusedWarnings ((==@#@$$) :: a6989586621679304361 -> TyFun a6989586621679304361 Bool -> *) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) # | |
type (==@#@$$$) (t :: a6989586621679304361) (t :: a6989586621679304361) = (==) t t #
data (/=@#@$) (l :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type)) #
Instances
| SuppressUnusedWarnings ((/=@#@$) :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type) -> *) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((/=@#@$) :: TyFun a6989586621679304361 (TyFun a6989586621679304361 Bool -> Type) -> *) (l :: a6989586621679304361) # | |
data (l :: a6989586621679304361) /=@#@$$ (l :: TyFun a6989586621679304361 Bool) #
Instances
| SuppressUnusedWarnings ((/=@#@$$) :: a6989586621679304361 -> TyFun a6989586621679304361 Bool -> *) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) # | |
type (/=@#@$$$) (t :: a6989586621679304361) (t :: a6989586621679304361) = (/=) t t #