Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.Core.Data.Class.SymEq

Contents

Symbolic equality
More Eq helper
Generic SymEq

Description

Synopsis

class SymEq a where
- (.==) :: a -> a -> SymBool
- (./=) :: a -> a -> SymBool
- symDistinct :: [a] -> SymBool
class (forall a. SymEq a => SymEq (f a)) => SymEq1 (f :: Type -> Type) where
- liftSymEq :: (a -> b -> SymBool) -> f a -> f b -> SymBool
symEq1 :: (SymEq a, SymEq1 f) => f a -> f a -> SymBool
class (forall a. SymEq a => SymEq1 (f a)) => SymEq2 (f :: Type -> Type -> Type) where
- liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
symEq2 :: (SymEq a, SymEq b, SymEq2 f) => f a b -> f a b -> SymBool
pairwiseSymDistinct :: SymEq a => [a] -> SymBool
distinct :: Eq a => [a] -> Bool
data family SymEqArgs arity a b
class GSymEq arity (f :: Type -> Type) where
- gsymEq :: SymEqArgs arity a b -> f a -> f b -> SymBool
genericSymEq :: (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool
genericLiftSymEq :: (Generic1 f, GSymEq Arity1 (Rep1 f)) => (a -> b -> SymBool) -> f a -> f b -> SymBool

Symbolic equality

class SymEq a where Source #

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

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

symDistinct :: [a] -> SymBool Source #

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

Instances

Instances details

SymEq ByteString Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: ByteString -> ByteString -> SymBool Source # (./=) :: ByteString -> ByteString -> SymBool Source # symDistinct :: [ByteString] -> SymBool Source #
SymEq All Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: All -> All -> SymBool Source # (./=) :: All -> All -> SymBool Source # symDistinct :: [All] -> SymBool Source #
SymEq Any Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Any -> Any -> SymBool Source # (./=) :: Any -> Any -> SymBool Source # symDistinct :: [Any] -> SymBool Source #
SymEq Int16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Int16 -> Int16 -> SymBool Source # (./=) :: Int16 -> Int16 -> SymBool Source # symDistinct :: [Int16] -> SymBool Source #
SymEq Int32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Int32 -> Int32 -> SymBool Source # (./=) :: Int32 -> Int32 -> SymBool Source # symDistinct :: [Int32] -> SymBool Source #
SymEq Int64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Int64 -> Int64 -> SymBool Source # (./=) :: Int64 -> Int64 -> SymBool Source # symDistinct :: [Int64] -> SymBool Source #
SymEq Int8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Int8 -> Int8 -> SymBool Source # (./=) :: Int8 -> Int8 -> SymBool Source # symDistinct :: [Int8] -> SymBool Source #
SymEq Word16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Word16 -> Word16 -> SymBool Source # (./=) :: Word16 -> Word16 -> SymBool Source # symDistinct :: [Word16] -> SymBool Source #
SymEq Word32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Word32 -> Word32 -> SymBool Source # (./=) :: Word32 -> Word32 -> SymBool Source # symDistinct :: [Word32] -> SymBool Source #
SymEq Word64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Word64 -> Word64 -> SymBool Source # (./=) :: Word64 -> Word64 -> SymBool Source # symDistinct :: [Word64] -> SymBool Source #
SymEq Word8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Word8 -> Word8 -> SymBool Source # (./=) :: Word8 -> Word8 -> SymBool Source # symDistinct :: [Word8] -> SymBool Source #
SymEq Ordering Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Ordering -> Ordering -> SymBool Source # (./=) :: Ordering -> Ordering -> SymBool Source # symDistinct :: [Ordering] -> SymBool Source #
SymEq AssertionError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: AssertionError -> AssertionError -> SymBool Source # (./=) :: AssertionError -> AssertionError -> SymBool Source # symDistinct :: [AssertionError] -> SymBool Source #
SymEq VerificationConditions Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: VerificationConditions -> VerificationConditions -> SymBool Source # (./=) :: VerificationConditions -> VerificationConditions -> SymBool Source # symDistinct :: [VerificationConditions] -> SymBool Source #
SymEq AlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: AlgReal -> AlgReal -> SymBool Source # (./=) :: AlgReal -> AlgReal -> SymBool Source # symDistinct :: [AlgReal] -> SymBool Source #
SymEq FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (./=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # symDistinct :: [FPRoundingMode] -> SymBool Source #
SymEq NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (./=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # symDistinct :: [NotRepresentableFPError] -> SymBool Source #
SymEq SomeBVException Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.==) :: SomeBVException -> SomeBVException -> SymBool Source # (./=) :: SomeBVException -> SomeBVException -> SymBool Source # symDistinct :: [SomeBVException] -> SymBool Source #
SymEq SymAlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymAlgReal -> SymAlgReal -> SymBool Source # (./=) :: SymAlgReal -> SymAlgReal -> SymBool Source # symDistinct :: [SymAlgReal] -> SymBool Source #
SymEq SymBool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymBool -> SymBool -> SymBool Source # (./=) :: SymBool -> SymBool -> SymBool Source # symDistinct :: [SymBool] -> SymBool Source #
SymEq SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source # (./=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source # symDistinct :: [SymFPRoundingMode] -> SymBool Source #
SymEq SymInteger Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymInteger -> SymInteger -> SymBool Source # (./=) :: SymInteger -> SymInteger -> SymBool Source # symDistinct :: [SymInteger] -> SymBool Source #
SymEq Text Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Text -> Text -> SymBool Source # (./=) :: Text -> Text -> SymBool Source # symDistinct :: [Text] -> SymBool Source #
SymEq Integer Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Integer -> Integer -> SymBool Source # (./=) :: Integer -> Integer -> SymBool Source # symDistinct :: [Integer] -> SymBool Source #
SymEq () Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: () -> () -> SymBool Source # (./=) :: () -> () -> SymBool Source # symDistinct :: [()] -> SymBool Source #
SymEq Bool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Bool -> Bool -> SymBool Source # (./=) :: Bool -> Bool -> SymBool Source # symDistinct :: [Bool] -> SymBool Source #
SymEq Char Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Char -> Char -> SymBool Source # (./=) :: Char -> Char -> SymBool Source # symDistinct :: [Char] -> SymBool Source #
SymEq Double Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Double -> Double -> SymBool Source # (./=) :: Double -> Double -> SymBool Source # symDistinct :: [Double] -> SymBool Source #
SymEq Float Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Float -> Float -> SymBool Source # (./=) :: Float -> Float -> SymBool Source # symDistinct :: [Float] -> SymBool Source #
SymEq Int Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Int -> Int -> SymBool Source # (./=) :: Int -> Int -> SymBool Source # symDistinct :: [Int] -> SymBool Source #
SymEq Word Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Word -> Word -> SymBool Source # (./=) :: Word -> Word -> SymBool Source # symDistinct :: [Word] -> SymBool Source #
(Generic a, GSymEq Arity0 (Rep a)) => SymEq (Default a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods (.==) :: Default a -> Default a -> SymBool Source # (./=) :: Default a -> Default a -> SymBool Source # symDistinct :: [Default a] -> SymBool Source #
SymEq a => SymEq (Identity a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Identity a -> Identity a -> SymBool Source # (./=) :: Identity a -> Identity a -> SymBool Source # symDistinct :: [Identity a] -> SymBool Source #
SymEq a => SymEq (First a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: First a -> First a -> SymBool Source # (./=) :: First a -> First a -> SymBool Source # symDistinct :: [First a] -> SymBool Source #
SymEq a => SymEq (Last a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Last a -> Last a -> SymBool Source # (./=) :: Last a -> Last a -> SymBool Source # symDistinct :: [Last a] -> SymBool Source #
SymEq a => SymEq (Down a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Down a -> Down a -> SymBool Source # (./=) :: Down a -> Down a -> SymBool Source # symDistinct :: [Down a] -> SymBool Source #
SymEq a => SymEq (Dual a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Dual a -> Dual a -> SymBool Source # (./=) :: Dual a -> Dual a -> SymBool Source # symDistinct :: [Dual a] -> SymBool Source #
SymEq a => SymEq (Product a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Product a -> Product a -> SymBool Source # (./=) :: Product a -> Product a -> SymBool Source # symDistinct :: [Product a] -> SymBool Source #
SymEq a => SymEq (Sum a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Sum a -> Sum a -> SymBool Source # (./=) :: Sum a -> Sum a -> SymBool Source # symDistinct :: [Sum a] -> SymBool Source #
SymEq p => SymEq (Par1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Par1 p -> Par1 p -> SymBool Source # (./=) :: Par1 p -> Par1 p -> SymBool Source # symDistinct :: [Par1 p] -> SymBool Source #
SymEq a => SymEq (Ratio a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Ratio a -> Ratio a -> SymBool Source # (./=) :: Ratio a -> Ratio a -> SymBool Source # symDistinct :: [Ratio a] -> SymBool Source #
SymEq a => SymEq (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods (.==) :: Union a -> Union a -> SymBool Source # (./=) :: Union a -> Union a -> SymBool Source # symDistinct :: [Union a] -> SymBool Source #
(KnownNat n, 1 <= n) => SymEq (IntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: IntN n -> IntN n -> SymBool Source # (./=) :: IntN n -> IntN n -> SymBool Source # symDistinct :: [IntN n] -> SymBool Source #
(KnownNat n, 1 <= n) => SymEq (WordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: WordN n -> WordN n -> SymBool Source # (./=) :: WordN n -> WordN n -> SymBool Source # symDistinct :: [WordN n] -> SymBool Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymEq (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SymEq (SomeBV bv) Source #	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`.
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.==) :: SomeBV bv -> SomeBV bv -> SymBool Source # (./=) :: SomeBV bv -> SomeBV bv -> SymBool Source # symDistinct :: [SomeBV bv] -> SymBool Source #
(KnownNat n, 1 <= n) => SymEq (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymIntN n -> SymIntN n -> SymBool Source # (./=) :: SymIntN n -> SymIntN n -> SymBool Source # symDistinct :: [SymIntN n] -> SymBool Source #
(KnownNat n, 1 <= n) => SymEq (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymWordN n -> SymWordN n -> SymBool Source # (./=) :: SymWordN n -> SymWordN n -> SymBool Source # symDistinct :: [SymWordN n] -> SymBool Source #
SymEq a => SymEq (Maybe a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Maybe a -> Maybe a -> SymBool Source # (./=) :: Maybe a -> Maybe a -> SymBool Source # symDistinct :: [Maybe a] -> SymBool Source #
SymEq a => SymEq [a] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: [a] -> [a] -> SymBool Source # (./=) :: [a] -> [a] -> SymBool Source # symDistinct :: [[a]] -> SymBool Source #
(Generic1 f, GSymEq Arity1 (Rep1 f), SymEq a) => SymEq (Default1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods (.==) :: Default1 f a -> Default1 f a -> SymBool Source # (./=) :: Default1 f a -> Default1 f a -> SymBool Source # symDistinct :: [Default1 f a] -> SymBool Source #
(SymEq a1, SymEq a2) => SymEq (Either a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Either a1 a2 -> Either a1 a2 -> SymBool Source # (./=) :: Either a1 a2 -> Either a1 a2 -> SymBool Source # symDistinct :: [Either a1 a2] -> SymBool Source #
SymEq (Proxy a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Proxy a -> Proxy a -> SymBool Source # (./=) :: Proxy a -> Proxy a -> SymBool Source # symDistinct :: [Proxy a] -> SymBool Source #
SymEq (U1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: U1 p -> U1 p -> SymBool Source # (./=) :: U1 p -> U1 p -> SymBool Source # symDistinct :: [U1 p] -> SymBool Source #
SymEq (V1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: V1 p -> V1 p -> SymBool Source # (./=) :: V1 p -> V1 p -> SymBool Source # symDistinct :: [V1 p] -> SymBool Source #
(SymEq e, SymEq a) => SymEq (CBMCEither e a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods (.==) :: CBMCEither e a -> CBMCEither e a -> SymBool Source # (./=) :: CBMCEither e a -> CBMCEither e a -> SymBool Source # symDistinct :: [CBMCEither e a] -> SymBool Source #
ValidFP eb sb => SymEq (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: FP eb sb -> FP eb sb -> SymBool Source # (./=) :: FP eb sb -> FP eb sb -> SymBool Source # symDistinct :: [FP eb sb] -> SymBool Source #
ValidFP eb sb => SymEq (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymFP eb sb -> SymFP eb sb -> SymBool Source # (./=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source # symDistinct :: [SymFP eb sb] -> SymBool Source #
(SymEq1 a1, SymEq a2) => SymEq (MaybeT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: MaybeT a1 a2 -> MaybeT a1 a2 -> SymBool Source # (./=) :: MaybeT a1 a2 -> MaybeT a1 a2 -> SymBool Source # symDistinct :: [MaybeT a1 a2] -> SymBool Source #
(SymEq a1, SymEq a2) => SymEq (a1, a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2) -> (a1, a2) -> SymBool Source # (./=) :: (a1, a2) -> (a1, a2) -> SymBool Source # symDistinct :: [(a1, a2)] -> SymBool Source #
SymEq a => SymEq (Const a b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Const a b -> Const a b -> SymBool Source # (./=) :: Const a b -> Const a b -> SymBool Source # symDistinct :: [Const a b] -> SymBool Source #
SymEq (f a) => SymEq (Ap f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Ap f a -> Ap f a -> SymBool Source # (./=) :: Ap f a -> Ap f a -> SymBool Source # symDistinct :: [Ap f a] -> SymBool Source #
SymEq (f a) => SymEq (Alt f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Alt f a -> Alt f a -> SymBool Source # (./=) :: Alt f a -> Alt f a -> SymBool Source # symDistinct :: [Alt f a] -> SymBool Source #
SymEq (f p) => SymEq (Rec1 f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Rec1 f p -> Rec1 f p -> SymBool Source # (./=) :: Rec1 f p -> Rec1 f p -> SymBool Source # symDistinct :: [Rec1 f p] -> SymBool Source #
SymEq (m (CBMCEither e a)) => SymEq (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods (.==) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (./=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # symDistinct :: [CBMCExceptT e m a] -> SymBool Source #
(SymEq a1, SymEq1 a2, SymEq a3) => SymEq (ExceptT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> SymBool Source # (./=) :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> SymBool Source # symDistinct :: [ExceptT a1 a2 a3] -> SymBool Source #
(SymEq1 m, SymEq a) => SymEq (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: IdentityT m a -> IdentityT m a -> SymBool Source # (./=) :: IdentityT m a -> IdentityT m a -> SymBool Source # symDistinct :: [IdentityT m a] -> SymBool Source #
(SymEq a1, SymEq1 a2, SymEq a3) => SymEq (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (./=) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # symDistinct :: [WriterT a1 a2 a3] -> SymBool Source #
(SymEq a1, SymEq1 a2, SymEq a3) => SymEq (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (./=) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # symDistinct :: [WriterT a1 a2 a3] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3) => SymEq (a1, a2, a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3) -> (a1, a2, a3) -> SymBool Source # (./=) :: (a1, a2, a3) -> (a1, a2, a3) -> SymBool Source # symDistinct :: [(a1, a2, a3)] -> SymBool Source #
(SymEq (l a), SymEq (r a)) => SymEq (Product l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Product l r a -> Product l r a -> SymBool Source # (./=) :: Product l r a -> Product l r a -> SymBool Source # symDistinct :: [Product l r a] -> SymBool Source #
(SymEq (l a), SymEq (r a)) => SymEq (Sum l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Sum l r a -> Sum l r a -> SymBool Source # (./=) :: Sum l r a -> Sum l r a -> SymBool Source # symDistinct :: [Sum l r a] -> SymBool Source #
(SymEq (f p), SymEq (g p)) => SymEq ((f :*: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (f :: g) p -> (f :: g) p -> SymBool Source # (./=) :: (f :: g) p -> (f :: g) p -> SymBool Source # symDistinct :: [(f :*: g) p] -> SymBool Source #
(SymEq (f p), SymEq (g p)) => SymEq ((f :+: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (f :+: g) p -> (f :+: g) p -> SymBool Source # (./=) :: (f :+: g) p -> (f :+: g) p -> SymBool Source # symDistinct :: [(f :+: g) p] -> SymBool Source #
SymEq c => SymEq (K1 i c p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: K1 i c p -> K1 i c p -> SymBool Source # (./=) :: K1 i c p -> K1 i c p -> SymBool Source # symDistinct :: [K1 i c p] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4) => SymEq (a1, a2, a3, a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> SymBool Source # (./=) :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4)] -> SymBool Source #
SymEq (f (g a)) => SymEq (Compose f g a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: Compose f g a -> Compose f g a -> SymBool Source # (./=) :: Compose f g a -> Compose f g a -> SymBool Source # symDistinct :: [Compose f g a] -> SymBool Source #
SymEq (f (g p)) => SymEq ((f :.: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (f :.: g) p -> (f :.: g) p -> SymBool Source # (./=) :: (f :.: g) p -> (f :.: g) p -> SymBool Source # symDistinct :: [(f :.: g) p] -> SymBool Source #
SymEq (f p) => SymEq (M1 i c f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: M1 i c f p -> M1 i c f p -> SymBool Source # (./=) :: M1 i c f p -> M1 i c f p -> SymBool Source # symDistinct :: [M1 i c f p] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5) => SymEq (a1, a2, a3, a4, a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6) => SymEq (a1, a2, a3, a4, a5, a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7) => SymEq (a1, a2, a3, a4, a5, a6, a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12, SymEq a13) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12, SymEq a13, SymEq a14) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14)] -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12, SymEq a13, SymEq a14, SymEq a15) => SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> SymBool Source # (./=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> SymBool Source # symDistinct :: [(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)] -> SymBool Source #

class (forall a. SymEq a => SymEq (f a)) => SymEq1 (f :: Type -> Type) where Source #

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

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

Instances details

SymEq1 Identity Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Identity a -> Identity b -> SymBool Source #
SymEq1 First Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> First a -> First b -> SymBool Source #
SymEq1 Last Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Last a -> Last b -> SymBool Source #
SymEq1 Down Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Down a -> Down b -> SymBool Source #
SymEq1 Dual Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Dual a -> Dual b -> SymBool Source #
SymEq1 Product Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Product a -> Product b -> SymBool Source #
SymEq1 Sum Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Sum a -> Sum b -> SymBool Source #
SymEq1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftSymEq :: (a -> b -> SymBool) -> Union a -> Union b -> SymBool Source #
SymEq1 Maybe Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Maybe a -> Maybe b -> SymBool Source #
SymEq1 [] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> [a] -> [b] -> SymBool Source #
(Generic1 f, GSymEq Arity1 (Rep1 f)) => SymEq1 (Default1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Default1 f a -> Default1 f b -> SymBool Source #
SymEq a => SymEq1 (Either a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a0 -> b -> SymBool) -> Either a a0 -> Either a b -> SymBool Source #
SymEq1 (Proxy :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Proxy a -> Proxy b -> SymBool Source #
SymEq1 a => SymEq1 (MaybeT a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a0 -> b -> SymBool) -> MaybeT a a0 -> MaybeT a b -> SymBool Source #
SymEq a => SymEq1 ((,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a0 -> b -> SymBool) -> (a, a0) -> (a, b) -> SymBool Source #
SymEq a => SymEq1 (Const a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a0 -> b -> SymBool) -> Const a a0 -> Const a b -> SymBool Source #
SymEq1 f => SymEq1 (Ap f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Ap f a -> Ap f b -> SymBool Source #
SymEq1 f => SymEq1 (Alt f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Alt f a -> Alt f b -> SymBool Source #
(SymEq a1, SymEq1 a2) => SymEq1 (ExceptT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> ExceptT a1 a2 a -> ExceptT a1 a2 b -> SymBool Source #
SymEq1 m => SymEq1 (IdentityT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> IdentityT m a -> IdentityT m b -> SymBool Source #
(SymEq a1, SymEq1 a2) => SymEq1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> WriterT a1 a2 a -> WriterT a1 a2 b -> SymBool Source #
(SymEq a1, SymEq1 a2) => SymEq1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> WriterT a1 a2 a -> WriterT a1 a2 b -> SymBool Source #
(SymEq a1, SymEq a2) => SymEq1 ((,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a) -> (a1, a2, b) -> SymBool Source #
(SymEq1 l, SymEq1 r) => SymEq1 (Product l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Product l r a -> Product l r b -> SymBool Source #
(SymEq1 l, SymEq1 r) => SymEq1 (Sum l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Sum l r a -> Sum l r b -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3) => SymEq1 ((,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a) -> (a1, a2, a3, b) -> SymBool Source #
(SymEq1 f, SymEq1 g) => SymEq1 (Compose f g) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> Compose f g a -> Compose f g b -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4) => SymEq1 ((,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a) -> (a1, a2, a3, a4, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5) => SymEq1 ((,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a) -> (a1, a2, a3, a4, a5, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6) => SymEq1 ((,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a) -> (a1, a2, a3, a4, a5, a6, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7) => SymEq1 ((,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a) -> (a1, a2, a3, a4, a5, a6, a7, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8) => SymEq1 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9) => SymEq1 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10) => SymEq1 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11) => SymEq1 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12) => SymEq1 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12, SymEq a13) => SymEq1 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, b) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12, SymEq a13, SymEq a14) => SymEq1 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq :: (a -> b -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, b) -> SymBool Source #

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

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

class (forall a. SymEq a => SymEq1 (f a)) => SymEq2 (f :: Type -> Type -> Type) where Source #

Lifting of the SymEq class to binary type constructors.

Methods

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

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

Instances details

SymEq2 Either Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> Either a c -> Either b d -> SymBool Source #
SymEq2 (,) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a, c) -> (b, d) -> SymBool Source #
SymEq a => SymEq2 ((,,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a0 -> b -> SymBool) -> (c -> d -> SymBool) -> (a, a0, c) -> (a, b, d) -> SymBool Source #
(SymEq a1, SymEq a2) => SymEq2 ((,,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a, c) -> (a1, a2, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3) => SymEq2 ((,,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a, c) -> (a1, a2, a3, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4) => SymEq2 ((,,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a, c) -> (a1, a2, a3, a4, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5) => SymEq2 ((,,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a, c) -> (a1, a2, a3, a4, a5, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6) => SymEq2 ((,,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a, c) -> (a1, a2, a3, a4, a5, a6, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7) => SymEq2 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a, c) -> (a1, a2, a3, a4, a5, a6, a7, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8) => SymEq2 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, c) -> (a1, a2, a3, a4, a5, a6, a7, a8, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9) => SymEq2 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, c) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10) => SymEq2 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, c) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11) => SymEq2 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, c) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12) => SymEq2 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, c) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, b, d) -> SymBool Source #
(SymEq a1, SymEq a2, SymEq a3, SymEq a4, SymEq a5, SymEq a6, SymEq a7, SymEq a8, SymEq a9, SymEq a10, SymEq a11, SymEq a12, SymEq a13) => SymEq2 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, c) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, b, d) -> SymBool Source #

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

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

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

Default pairwise symbolic distinct implementation.

More `Eq` helper

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

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

The arguments to the generic equality function.

Instances

Instances details

data SymEqArgs Arity0 _ _1 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq data SymEqArgs Arity0 _ _1 = SymEqArgs0
newtype SymEqArgs Arity1 a b Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq newtype SymEqArgs Arity1 a b = SymEqArgs1 (a -> b -> SymBool)

class GSymEq arity (f :: Type -> Type) where Source #

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

Methods

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

Instances

Instances details

GSymEq Arity1 Par1 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs Arity1 a b -> Par1 a -> Par1 b -> SymBool Source #
GSymEq arity (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs arity a b -> U1 a -> U1 b -> SymBool Source #
GSymEq arity (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs arity a b -> V1 a -> V1 b -> SymBool Source #
SymEq1 f => GSymEq Arity1 (Rec1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs Arity1 a b -> Rec1 f a -> Rec1 f b -> SymBool Source #
(GSymEq arity a, GSymEq arity b) => GSymEq arity (a :*: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs arity a0 b0 -> (a :: b) a0 -> (a :: b) b0 -> SymBool Source #
(GSymEq arity a, GSymEq arity b) => GSymEq arity (a :+: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs arity a0 b0 -> (a :+: b) a0 -> (a :+: b) b0 -> SymBool Source #
SymEq a => GSymEq arity (K1 i a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs arity a0 b -> K1 i a a0 -> K1 i a b -> SymBool Source #
(SymEq1 f, GSymEq Arity1 g) => GSymEq Arity1 (f :.: g) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs Arity1 a b -> (f :.: g) a -> (f :.: g) b -> SymBool Source #
GSymEq arity a => GSymEq arity (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq Methods gsymEq :: SymEqArgs arity a0 b -> M1 i c a a0 -> M1 i c a b -> SymBool Source #

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

Generic (.==) function.

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

Generic liftSymEq function.

Symbolic equality

Instances

Instances

Instances

More Eq helper

Generic SymEq

Instances

Instances

More `Eq` helper

Generic `SymEq`