Grisette.Internal.Core.Data.Class.SymEq

Symbolic equality

class SymEq 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
(distinct 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 SymEq via (Default X)

Minimal complete definition

(.==) | (./=)

Methods

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

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

symDistinct :: [a] -> SymBool

Check if all elements in a list are distinct, under the symbolic equality semantics.

Instances

SymEq All

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [All] -> SymBool

SymEq Any

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Any] -> SymBool

SymEq Int16

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Int16] -> SymBool

SymEq Int32

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Int32] -> SymBool

SymEq Int64

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Int64] -> SymBool

SymEq Int8

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Int8] -> SymBool

SymEq Word16

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Word16] -> SymBool

SymEq Word32

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Word32] -> SymBool

SymEq Word64

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Word64] -> SymBool

SymEq Word8

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Word8] -> SymBool

SymEq ByteString

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [ByteString] -> SymBool

SymEq Ordering

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Ordering] -> SymBool

SymEq AssertionError

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [AssertionError] -> SymBool

SymEq VerificationConditions

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [VerificationConditions] -> SymBool

SymEq AlgReal

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [AlgReal] -> SymBool

SymEq FPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [FPRoundingMode] -> SymBool

SymEq NotRepresentableFPError

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [NotRepresentableFPError] -> SymBool

SymEq SomeBVException

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

symDistinct :: [SomeBVException] -> SymBool

SymEq SymAlgReal

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymAlgReal] -> SymBool

SymEq SymBool

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymBool] -> SymBool

SymEq SymFPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymFPRoundingMode] -> SymBool

SymEq SymInteger

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymInteger] -> SymBool

SymEq Text

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Text] -> SymBool

SymEq Integer

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Integer] -> SymBool

SymEq ()

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [()] -> SymBool

SymEq Bool

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Bool] -> SymBool

SymEq Char

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Char] -> SymBool

SymEq Double

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Double] -> SymBool

SymEq Float

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Float] -> SymBool

SymEq Int

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Int] -> SymBool

SymEq Word

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Word] -> SymBool

SymEq a => SymEq (Identity a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Identity a] -> SymBool

SymEq a => SymEq (First a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [First a] -> SymBool

SymEq a => SymEq (Last a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Last a] -> SymBool

SymEq a => SymEq (Down a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Down a] -> SymBool

SymEq a => SymEq (Dual a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Dual a] -> SymBool

SymEq a => SymEq (Product a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Product a] -> SymBool

SymEq a => SymEq (Sum a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Sum a] -> SymBool

SymEq p => SymEq (Par1 p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Par1 p] -> SymBool

SymEq a => SymEq (Ratio a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Ratio a] -> SymBool

(Generic a, GSymEq Arity0 (Rep a)) => SymEq (Default a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Default a] -> SymBool

SymEq a => SymEq (Union a)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

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

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

symDistinct :: [Union a] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [IntN n] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [WordN n] -> SymBool

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymEq (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => SymEq (SomeBV bv)

The symDistinct instance for SomeBV will have the following behavior:

• If the list is empty or has only one element, it will return True.
• If none of the elements have a bit-width, it will throw UndeterminedBitwidth exception.
• If the elements have different bit-widths, it will throw a BitwidthMismatch exception.
• If there are at least one element have a bit-width, and all elements with known bit-width have the same bit-width, it will generate a single symbolic formula using distinct.

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

symDistinct :: [SomeBV bv] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymIntN n] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymWordN n] -> SymBool

SymEq a => SymEq (Maybe a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Maybe a] -> SymBool

SymEq a => SymEq [a]

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [[a]] -> SymBool

(SymEq a, SymEq b) => SymEq (Either a b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Either a b] -> SymBool

SymEq (U1 p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [U1 p] -> SymBool

SymEq (V1 p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [V1 p] -> SymBool

(Generic1 f, GSymEq Arity1 (Rep1 f), SymEq a) => SymEq (Default1 f a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: Default1 f a -> Default1 f a -> SymBool

(./=) :: Default1 f a -> Default1 f a -> SymBool

symDistinct :: [Default1 f a] -> SymBool

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

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

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

symDistinct :: [CBMCEither e a] -> SymBool

ValidFP eb sb => SymEq (FP eb sb)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: FP eb sb -> FP eb sb -> SymBool

(./=) :: FP eb sb -> FP eb sb -> SymBool

symDistinct :: [FP eb sb] -> SymBool

ValidFP eb sb => SymEq (SymFP eb sb)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: SymFP eb sb -> SymFP eb sb -> SymBool

(./=) :: SymFP eb sb -> SymFP eb sb -> SymBool

symDistinct :: [SymFP eb sb] -> SymBool

(SymEq1 m, SymEq a) => SymEq (MaybeT m a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [MaybeT m a] -> SymBool

(SymEq a, SymEq b) => SymEq (a, b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b)] -> SymBool

SymEq a => SymEq (Const a b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Const a b] -> SymBool

SymEq (f a) => SymEq (Ap f a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: Ap f a -> Ap f a -> SymBool

(./=) :: Ap f a -> Ap f a -> SymBool

symDistinct :: [Ap f a] -> SymBool

SymEq (f a) => SymEq (Alt f a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: Alt f a -> Alt f a -> SymBool

(./=) :: Alt f a -> Alt f a -> SymBool

symDistinct :: [Alt f a] -> SymBool

SymEq (f p) => SymEq (Rec1 f p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: Rec1 f p -> Rec1 f p -> SymBool

(./=) :: Rec1 f p -> Rec1 f p -> SymBool

symDistinct :: [Rec1 f p] -> SymBool

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

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

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

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

symDistinct :: [CBMCExceptT e m a] -> SymBool

(SymEq1 m, SymEq e, SymEq a) => SymEq (ExceptT e m a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [ExceptT e m a] -> SymBool

(SymEq1 m, SymEq a) => SymEq (IdentityT m a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [IdentityT m a] -> SymBool

(SymEq1 m, SymEq w, SymEq a) => SymEq (WriterT w m a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [WriterT w m a] -> SymBool

(SymEq1 m, SymEq w, SymEq a) => SymEq (WriterT w m a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [WriterT w m a] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c)] -> SymBool

(SymEq (l a), SymEq (r a)) => SymEq (Product l r a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: Product l r a -> Product l r a -> SymBool

(./=) :: Product l r a -> Product l r a -> SymBool

symDistinct :: [Product l r a] -> SymBool

(SymEq (l a), SymEq (r a)) => SymEq (Sum l r a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: Sum l r a -> Sum l r a -> SymBool

(./=) :: Sum l r a -> Sum l r a -> SymBool

symDistinct :: [Sum l r a] -> SymBool

(SymEq (f p), SymEq (g p)) => SymEq ((f :*: g) p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: (f :*: g) p -> (f :*: g) p -> SymBool

(./=) :: (f :*: g) p -> (f :*: g) p -> SymBool

symDistinct :: [(f :*: g) p] -> SymBool

(SymEq (f p), SymEq (g p)) => SymEq ((f :+: g) p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: (f :+: g) p -> (f :+: g) p -> SymBool

(./=) :: (f :+: g) p -> (f :+: g) p -> SymBool

symDistinct :: [(f :+: g) p] -> SymBool

SymEq c => SymEq (K1 i c p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

(./=) :: K1 i c p -> K1 i c p -> SymBool

symDistinct :: [K1 i c p] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c, d)] -> SymBool

SymEq (f (g a)) => SymEq (Compose f g a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [Compose f g a] -> SymBool

SymEq (f (g p)) => SymEq ((f :.: g) p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: (f :.: g) p -> (f :.: g) p -> SymBool

(./=) :: (f :.: g) p -> (f :.: g) p -> SymBool

symDistinct :: [(f :.: g) p] -> SymBool

SymEq (f p) => SymEq (M1 i c f p)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: M1 i c f p -> M1 i c f p -> SymBool

(./=) :: M1 i c f p -> M1 i c f p -> SymBool

symDistinct :: [M1 i c f p] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c, d, e)] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

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

symDistinct :: [(a, b, c, d, e, f)] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

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

symDistinct :: [(a, b, c, d, e, f, g)] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

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

symDistinct :: [(a, b, c, d, e, f, g, h)] -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c, d, e, f, g, h, i)] -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j) => SymEq (a, b, c, d, e, f, g, h, i, j)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c, d, e, f, g, h, i, j)] -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k) => SymEq (a, b, c, d, e, f, g, h, i, j, k)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c, d, e, f, g, h, i, j, k)] -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l) => SymEq (a, b, c, d, e, f, g, h, i, j, k, l)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [(a, b, c, d, e, f, g, h, i, j, k, l)] -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l, SymEq m) => SymEq (a, b, c, d, e, f, g, h, i, j, k, l, m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: (a, b, c, d, e, f, g, h, i, j, k, l, m) -> (a, b, c, d, e, f, g, h, i, j, k, l, m) -> SymBool

(./=) :: (a, b, c, d, e, f, g, h, i, j, k, l, m) -> (a, b, c, d, e, f, g, h, i, j, k, l, m) -> SymBool

symDistinct :: [(a, b, c, d, e, f, g, h, i, j, k, l, m)] -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l, SymEq m, SymEq n) => SymEq (a, b, c, d, e, f, g, h, i, j, k, l, m, n)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> SymBool

(./=) :: (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> SymBool

symDistinct :: [(a, b, c, d, e, f, g, h, i, j, k, l, m, n)] -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l, SymEq m, SymEq n, SymEq o) => SymEq (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

(.==) :: (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> SymBool

(./=) :: (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> SymBool

symDistinct :: [(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)] -> SymBool

class (forall a. SymEq a => SymEq (f a)) => SymEq1 f where

Lifting of the SymEq class to unary type constructors.

Any instance should be subject to the following law that canonicity is preserved:

liftSymEq (.==) should be equivalent to (.==), under the symbolic semantics.

This class therefore represents the generalization of SymEq by decomposing its main method into a canonical lifting on a canonical inner method, so that the lifting can be reused for other arguments than the canonical one.

Methods

liftSymEq :: (a -> b -> SymBool) -> f a -> f b -> SymBool

Lift a symbolic equality test through the type constructor.

The function will usually be applied to an symbolic equality function, but the more general type ensures that the implementation uses it to compare elements of the first container with elements of the second.

Instances

SymEq1 Identity

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Identity a -> Identity b -> SymBool

SymEq1 First

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> First a -> First b -> SymBool

SymEq1 Last

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Last a -> Last b -> SymBool

SymEq1 Down

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Down a -> Down b -> SymBool

SymEq1 Dual

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Dual a -> Dual b -> SymBool

SymEq1 Product

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Product a -> Product b -> SymBool

SymEq1 Sum

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Sum a -> Sum b -> SymBool

SymEq1 Union

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

liftSymEq :: (a -> b -> SymBool) -> Union a -> Union b -> SymBool

SymEq1 Maybe

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Maybe a -> Maybe b -> SymBool

SymEq1 List

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> [a] -> [b] -> SymBool

SymEq a => SymEq1 (Either a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b -> SymBool) -> Either a a0 -> Either a b -> SymBool

(Generic1 f, GSymEq Arity1 (Rep1 f)) => SymEq1 (Default1 f)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Default1 f a -> Default1 f b -> SymBool

SymEq1 m => SymEq1 (MaybeT m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> MaybeT m a -> MaybeT m b -> SymBool

SymEq a => SymEq1 ((,) a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b -> SymBool) -> (a, a0) -> (a, b) -> SymBool

SymEq a => SymEq1 (Const a :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b -> SymBool) -> Const a a0 -> Const a b -> SymBool

SymEq1 f => SymEq1 (Ap f)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Ap f a -> Ap f b -> SymBool

SymEq1 f => SymEq1 (Alt f)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Alt f a -> Alt f b -> SymBool

(SymEq1 m, SymEq e) => SymEq1 (ExceptT e m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> ExceptT e m a -> ExceptT e m b -> SymBool

SymEq1 m => SymEq1 (IdentityT m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> IdentityT m a -> IdentityT m b -> SymBool

(SymEq1 m, SymEq w) => SymEq1 (WriterT w m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> WriterT w m a -> WriterT w m b -> SymBool

(SymEq1 m, SymEq w) => SymEq1 (WriterT w m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> WriterT w m a -> WriterT w m b -> SymBool

(SymEq a, SymEq b) => SymEq1 ((,,) a b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, a0) -> (a, b, b0) -> SymBool

(SymEq1 l, SymEq1 r) => SymEq1 (Product l r)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Product l r a -> Product l r b -> SymBool

(SymEq1 l, SymEq1 r) => SymEq1 (Sum l r)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Sum l r a -> Sum l r b -> SymBool

(SymEq a, SymEq b, SymEq c) => SymEq1 ((,,,) a b c)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, a0) -> (a, b, c, b0) -> SymBool

(SymEq1 f, SymEq1 g) => SymEq1 (Compose f g)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a -> b -> SymBool) -> Compose f g a -> Compose f g b -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d) => SymEq1 ((,,,,) a b c d)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, a0) -> (a, b, c, d, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e) => SymEq1 ((,,,,,) a b c d e)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, a0) -> (a, b, c, d, e, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f) => SymEq1 ((,,,,,,) a b c d e f)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, a0) -> (a, b, c, d, e, f, b0) -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, a0) -> (a, b, c, d, e, f, g, b0) -> SymBool

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

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, a0) -> (a, b, c, d, e, f, g, h, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i) => SymEq1 ((,,,,,,,,,) a b c d e f g h i)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, i, a0) -> (a, b, c, d, e, f, g, h, i, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j) => SymEq1 ((,,,,,,,,,,) a b c d e f g h i j)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, i, j, a0) -> (a, b, c, d, e, f, g, h, i, j, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k) => SymEq1 ((,,,,,,,,,,,) a b c d e f g h i j k)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, i, j, k, a0) -> (a, b, c, d, e, f, g, h, i, j, k, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l) => SymEq1 ((,,,,,,,,,,,,) a b c d e f g h i j k l)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, i, j, k, l, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l, SymEq m) => SymEq1 ((,,,,,,,,,,,,,) a b c d e f g h i j k l m)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, b0) -> SymBool

(SymEq a, SymEq b, SymEq c, SymEq d, SymEq e, SymEq f, SymEq g, SymEq h, SymEq i, SymEq j, SymEq k, SymEq l, SymEq m, SymEq n) => SymEq1 ((,,,,,,,,,,,,,,) a b c d e f g h i j k l m n)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq :: (a0 -> b0 -> SymBool) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, b0) -> SymBool

symEq1 :: (SymEq a, SymEq1 f) => f a -> f a -> SymBool

Lift the standard (.==) function through the type constructor.

class (forall a. SymEq a => SymEq1 (f a)) => SymEq2 f where

Lifting of the SymEq class to binary type constructors.

Methods

liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> f a c -> f b d -> SymBool

Lift symbolic equality tests through the type constructor.

The function will usually be applied to an symbolic equality function, but the more general type ensures that the implementation uses it to compare elements of the first container with elements of the second.

Instances

SymEq2 Either

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> Either a c -> Either b d -> SymBool

SymEq2 (,)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a, c) -> (b, d) -> SymBool

SymEq a => SymEq2 ((,,) a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq2 :: (a0 -> b -> SymBool) -> (c -> d -> SymBool) -> (a, a0, c) -> (a, b, d) -> SymBool

(SymEq a, SymEq b) => SymEq2 ((,,,) a b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

liftSymEq2 :: (a0 -> b0 -> SymBool) -> (c -> d -> SymBool) -> (a, b, a0, c) -> (a, b, b0, d) -> SymBool

symEq2 :: (SymEq a, SymEq b, SymEq2 f) => f a b -> f a b -> SymBool

Lift the standard (.==) function through the type constructor.

pairwiseSymDistinct :: SymEq a => [a] -> SymBool

Default pairwise symbolic distinct implementation.

More Eq helper

distinct :: Eq a => [a] -> Bool

Check if all elements in a list are distinct.

Note that empty or singleton lists are always distinct.

>>> distinct []
True
>>> distinct [1]
True
>>> distinct [1, 2, 3]
True
>>> distinct [1, 2, 2]
False

Generic SymEq

data family SymEqArgs arity a b :: Type

The arguments to the generic equality function.

Instances

data SymEqArgs Arity0 _ _1

Defined in Grisette.Internal.Core.Data.Class.SymEq

data SymEqArgs Arity0 _ _1 = SymEqArgs0

newtype SymEqArgs Arity1 a b

Defined in Grisette.Internal.Core.Data.Class.SymEq

newtype SymEqArgs Arity1 a b = SymEqArgs1 (a -> b -> SymBool)

class GSymEq arity f where

The class of types that can be generically compared for symbolic equality.

Methods

gsymEq :: SymEqArgs arity a b -> f a -> f b -> SymBool

Instances

GSymEq Arity1 Par1

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs Arity1 a b -> Par1 a -> Par1 b -> SymBool

GSymEq arity (U1 :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs arity a b -> U1 a -> U1 b -> SymBool

GSymEq arity (V1 :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs arity a b -> V1 a -> V1 b -> SymBool

SymEq1 f => GSymEq Arity1 (Rec1 f)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs Arity1 a b -> Rec1 f a -> Rec1 f b -> SymBool

(GSymEq arity a, GSymEq arity b) => GSymEq arity (a :*: b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs arity a0 b0 -> (a :*: b) a0 -> (a :*: b) b0 -> SymBool

(GSymEq arity a, GSymEq arity b) => GSymEq arity (a :+: b)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs arity a0 b0 -> (a :+: b) a0 -> (a :+: b) b0 -> SymBool

SymEq a => GSymEq arity (K1 i a :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs arity a0 b -> K1 i a a0 -> K1 i a b -> SymBool

(SymEq1 f, GSymEq Arity1 g) => GSymEq Arity1 (f :.: g)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs Arity1 a b -> (f :.: g) a -> (f :.: g) b -> SymBool

GSymEq arity a => GSymEq arity (M1 i c a)

Defined in Grisette.Internal.Core.Data.Class.SymEq

Methods

gsymEq :: SymEqArgs arity a0 b -> M1 i c a a0 -> M1 i c a b -> SymBool

genericSymEq :: (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool

Generic (.==) function.

genericLiftSymEq :: (Generic1 f, GSymEq Arity1 (Rep1 f)) => (a -> b -> SymBool) -> f a -> f b -> SymBool

Generic liftSymEq function.