Grisette.Core.Data.Class.SEq

Symbolic equality

class SEq a where

Symbolic equality. Note that we can't use Haskell's Eq class since symbolic comparison won't necessarily return a concrete Bool value.

>>> let a = 1 :: SymInteger
>>> let b = 2 :: SymInteger
>>> a .== b
false
>>> a ./= b
true

>>> let a = "a" :: SymInteger
>>> let b = "b" :: SymInteger
>>> a ./= b
(! (= a b))
>>> a ./= b
(! (= a b))

Note: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extensions.

data X = ... deriving Generic deriving SEq via (Default X)

Minimal complete definition

(.==) | (./=)

Methods

(.==) :: a -> a -> SymBool infix 4

(./=) :: a -> a -> SymBool infix 4

Instances

SEq Int16

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Int16 -> Int16 -> SymBool

(./=) :: Int16 -> Int16 -> SymBool

SEq Int32

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Int32 -> Int32 -> SymBool

(./=) :: Int32 -> Int32 -> SymBool

SEq Int64

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Int64 -> Int64 -> SymBool

(./=) :: Int64 -> Int64 -> SymBool

SEq Int8

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Int8 -> Int8 -> SymBool

(./=) :: Int8 -> Int8 -> SymBool

SEq Word16

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Word16 -> Word16 -> SymBool

(./=) :: Word16 -> Word16 -> SymBool

SEq Word32

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Word32 -> Word32 -> SymBool

(./=) :: Word32 -> Word32 -> SymBool

SEq Word64

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Word64 -> Word64 -> SymBool

(./=) :: Word64 -> Word64 -> SymBool

SEq Word8

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Word8 -> Word8 -> SymBool

(./=) :: Word8 -> Word8 -> SymBool

SEq ByteString

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: ByteString -> ByteString -> SymBool

(./=) :: ByteString -> ByteString -> SymBool

SEq AssertionError

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: AssertionError -> AssertionError -> SymBool

(./=) :: AssertionError -> AssertionError -> SymBool

SEq VerificationConditions

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: VerificationConditions -> VerificationConditions -> SymBool

(./=) :: VerificationConditions -> VerificationConditions -> SymBool

SEq SomeIntN

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SomeIntN -> SomeIntN -> SymBool

(./=) :: SomeIntN -> SomeIntN -> SymBool

SEq SomeWordN

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SomeWordN -> SomeWordN -> SymBool

(./=) :: SomeWordN -> SomeWordN -> SymBool

SEq SomeSymIntN

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SomeSymIntN -> SomeSymIntN -> SymBool

(./=) :: SomeSymIntN -> SomeSymIntN -> SymBool

SEq SomeSymWordN

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SomeSymWordN -> SomeSymWordN -> SymBool

(./=) :: SomeSymWordN -> SomeSymWordN -> SymBool

SEq SymBool

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SymBool -> SymBool -> SymBool

(./=) :: SymBool -> SymBool -> SymBool

SEq SymInteger

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SymInteger -> SymInteger -> SymBool

(./=) :: SymInteger -> SymInteger -> SymBool

SEq Text

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Text -> Text -> SymBool

(./=) :: Text -> Text -> SymBool

SEq Integer

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Integer -> Integer -> SymBool

(./=) :: Integer -> Integer -> SymBool

SEq ()

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: () -> () -> SymBool

(./=) :: () -> () -> SymBool

SEq Bool

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Bool -> Bool -> SymBool

(./=) :: Bool -> Bool -> SymBool

SEq Char

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Char -> Char -> SymBool

(./=) :: Char -> Char -> SymBool

SEq Int

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Int -> Int -> SymBool

(./=) :: Int -> Int -> SymBool

SEq Word

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Word -> Word -> SymBool

(./=) :: Word -> Word -> SymBool

SEq a => SEq (Identity a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Identity a -> Identity a -> SymBool

(./=) :: Identity a -> Identity a -> SymBool

(Generic a, SEq' (Rep a)) => SEq (Default a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Default a -> Default a -> SymBool

(./=) :: Default a -> Default a -> SymBool

SEq a => SEq (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(.==) :: UnionM a -> UnionM a -> SymBool

(./=) :: UnionM a -> UnionM a -> SymBool

(KnownNat n, 1 <= n) => SEq (IntN n)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: IntN n -> IntN n -> SymBool

(./=) :: IntN n -> IntN n -> SymBool

(KnownNat n, 1 <= n) => SEq (WordN n)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: WordN n -> WordN n -> SymBool

(./=) :: WordN n -> WordN n -> SymBool

(KnownNat n, 1 <= n) => SEq (SymIntN n)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SymIntN n -> SymIntN n -> SymBool

(./=) :: SymIntN n -> SymIntN n -> SymBool

(KnownNat n, 1 <= n) => SEq (SymWordN n)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: SymWordN n -> SymWordN n -> SymBool

(./=) :: SymWordN n -> SymWordN n -> SymBool

SEq a => SEq (Maybe a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Maybe a -> Maybe a -> SymBool

(./=) :: Maybe a -> Maybe a -> SymBool

SEq a => SEq [a]

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: [a] -> [a] -> SymBool

(./=) :: [a] -> [a] -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Either e a -> Either e a -> SymBool

(./=) :: Either e a -> Either e a -> SymBool

(SEq e, SEq a) => SEq (CBMCEither e a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(.==) :: CBMCEither e a -> CBMCEither e a -> SymBool

(./=) :: CBMCEither e a -> CBMCEither e a -> SymBool

SEq (m (Maybe a)) => SEq (MaybeT m a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: MaybeT m a -> MaybeT m a -> SymBool

(./=) :: MaybeT m a -> MaybeT m a -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b) -> (a, b) -> SymBool

(./=) :: (a, b) -> (a, b) -> SymBool

SEq (m (CBMCEither e a)) => SEq (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(.==) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(./=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

SEq (m (Either e a)) => SEq (ExceptT e m a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: ExceptT e m a -> ExceptT e m a -> SymBool

(./=) :: ExceptT e m a -> ExceptT e m a -> SymBool

SEq (m a) => SEq (IdentityT m a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: IdentityT m a -> IdentityT m a -> SymBool

(./=) :: IdentityT m a -> IdentityT m a -> SymBool

SEq (m (a, s)) => SEq (WriterT s m a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: WriterT s m a -> WriterT s m a -> SymBool

(./=) :: WriterT s m a -> WriterT s m a -> SymBool

SEq (m (a, s)) => SEq (WriterT s m a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: WriterT s m a -> WriterT s m a -> SymBool

(./=) :: WriterT s m a -> WriterT s m a -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b, c) -> (a, b, c) -> SymBool

(./=) :: (a, b, c) -> (a, b, c) -> SymBool

(SEq (f a), SEq (g a)) => SEq (Sum f g a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: Sum f g a -> Sum f g a -> SymBool

(./=) :: Sum f g a -> Sum f g a -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b, c, d) -> (a, b, c, d) -> SymBool

(./=) :: (a, b, c, d) -> (a, b, c, d) -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool

(./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool

(./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool

(./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool

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

Defined in Grisette.Core.Data.Class.SEq

Methods

(.==) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool

(./=) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool

class SEq' f where

Auxiliary class for SEq instance derivation

Methods

(..==) :: f a -> f a -> SymBool infix 4

Auxiliary function for '(..==) derivation

Instances

SEq' (U1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.SEq

Methods

(..==) :: U1 a -> U1 a -> SymBool

SEq' (V1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.SEq

Methods

(..==) :: V1 a -> V1 a -> SymBool

(SEq' a, SEq' b) => SEq' (a :*: b)

Defined in Grisette.Core.Data.Class.SEq

Methods

(..==) :: (a :*: b) a0 -> (a :*: b) a0 -> SymBool

(SEq' a, SEq' b) => SEq' (a :+: b)

Defined in Grisette.Core.Data.Class.SEq

Methods

(..==) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool

SEq c => SEq' (K1 i c :: Type -> Type)

Defined in Grisette.Core.Data.Class.SEq

Methods

(..==) :: K1 i c a -> K1 i c a -> SymBool

SEq' a => SEq' (M1 i c a)

Defined in Grisette.Core.Data.Class.SEq

Methods

(..==) :: M1 i c a a0 -> M1 i c a a0 -> SymBool