Grisette.Internal.Core.Data.Class.SymOrd

Symbolic total order relation

class SymEq a => SymOrd a where

Symbolic total order. Note that we can't use Haskell's Ord class since symbolic comparison won't necessarily return a concrete Bool or Ordering value.

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

>>> let a = "a" :: SymInteger
>>> let b = "b" :: SymInteger
>>> a .< b
(< a b)
>>> a .<= b
(<= a b)
>>> a .> b
(< b a)
>>> a .>= b
(<= b a)

For symCompare, Ordering is not a solvable type, and the result would be wrapped in a union-like monad. See Union and PlainUnion for more information.

>>> a `symCompare` b :: Union Ordering
{If (< a b) LT (If (= a b) EQ GT)}

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

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

Minimal complete definition

(.<) | symCompare

Methods

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

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

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

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

symCompare :: a -> a -> Union Ordering

Instances

SymOrd All

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

Methods

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

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

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

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

symCompare :: All -> All -> Union Ordering

SymOrd Any

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

Methods

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

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

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

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

symCompare :: Any -> Any -> Union Ordering

SymOrd Int16

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

Methods

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

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

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

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

symCompare :: Int16 -> Int16 -> Union Ordering

SymOrd Int32

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

Methods

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

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

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

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

symCompare :: Int32 -> Int32 -> Union Ordering

SymOrd Int64

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

Methods

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

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

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

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

symCompare :: Int64 -> Int64 -> Union Ordering

SymOrd Int8

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

Methods

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

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

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

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

symCompare :: Int8 -> Int8 -> Union Ordering

SymOrd Word16

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

Methods

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

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

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

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

symCompare :: Word16 -> Word16 -> Union Ordering

SymOrd Word32

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

Methods

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

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

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

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

symCompare :: Word32 -> Word32 -> Union Ordering

SymOrd Word64

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

Methods

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

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

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

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

symCompare :: Word64 -> Word64 -> Union Ordering

SymOrd Word8

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

Methods

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

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

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

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

symCompare :: Word8 -> Word8 -> Union Ordering

SymOrd ByteString

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

Methods

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

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

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

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

symCompare :: ByteString -> ByteString -> Union Ordering

SymOrd Ordering

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

Methods

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

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

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

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

symCompare :: Ordering -> Ordering -> Union Ordering

SymOrd AssertionError

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

Methods

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

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

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

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

symCompare :: AssertionError -> AssertionError -> Union Ordering

SymOrd VerificationConditions

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

Methods

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

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

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

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

symCompare :: VerificationConditions -> VerificationConditions -> Union Ordering

SymOrd AlgReal

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

Methods

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

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

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

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

symCompare :: AlgReal -> AlgReal -> Union Ordering

SymOrd FPRoundingMode

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

Methods

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

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

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

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

symCompare :: FPRoundingMode -> FPRoundingMode -> Union Ordering

SymOrd NotRepresentableFPError

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

Methods

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

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

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

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

symCompare :: NotRepresentableFPError -> NotRepresentableFPError -> Union Ordering

SymOrd SomeBVException

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

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

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

symCompare :: SomeBVException -> SomeBVException -> Union Ordering

SymOrd SymAlgReal

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

Methods

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

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

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

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

symCompare :: SymAlgReal -> SymAlgReal -> Union Ordering

SymOrd SymBool

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

Methods

(.<) :: SymBool -> SymBool -> SymBool

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

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

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

symCompare :: SymBool -> SymBool -> Union Ordering

SymOrd SymFPRoundingMode

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

Methods

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

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

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

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

symCompare :: SymFPRoundingMode -> SymFPRoundingMode -> Union Ordering

SymOrd SymInteger

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

Methods

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

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

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

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

symCompare :: SymInteger -> SymInteger -> Union Ordering

SymOrd Text

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

Methods

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

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

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

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

symCompare :: Text -> Text -> Union Ordering

SymOrd Integer

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

Methods

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

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

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

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

symCompare :: Integer -> Integer -> Union Ordering

SymOrd ()

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

Methods

(.<) :: () -> () -> SymBool

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

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

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

symCompare :: () -> () -> Union Ordering

SymOrd Bool

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

Methods

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

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

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

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

symCompare :: Bool -> Bool -> Union Ordering

SymOrd Char

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

Methods

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

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

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

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

symCompare :: Char -> Char -> Union Ordering

SymOrd Double

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

Methods

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

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

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

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

symCompare :: Double -> Double -> Union Ordering

SymOrd Float

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

Methods

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

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

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

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

symCompare :: Float -> Float -> Union Ordering

SymOrd Int

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

Methods

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

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

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

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

symCompare :: Int -> Int -> Union Ordering

SymOrd Word

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

Methods

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

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

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

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

symCompare :: Word -> Word -> Union Ordering

SymOrd a => SymOrd (Identity a)

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

Methods

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

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

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

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

symCompare :: Identity a -> Identity a -> Union Ordering

SymOrd a => SymOrd (First a)

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

Methods

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

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

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

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

symCompare :: First a -> First a -> Union Ordering

SymOrd a => SymOrd (Last a)

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

Methods

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

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

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

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

symCompare :: Last a -> Last a -> Union Ordering

SymOrd a => SymOrd (Down a)

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

Methods

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

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

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

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

symCompare :: Down a -> Down a -> Union Ordering

SymOrd a => SymOrd (Dual a)

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

Methods

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

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

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

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

symCompare :: Dual a -> Dual a -> Union Ordering

SymOrd a => SymOrd (Product a)

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

Methods

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

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

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

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

symCompare :: Product a -> Product a -> Union Ordering

SymOrd a => SymOrd (Sum a)

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

Methods

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

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

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

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

symCompare :: Sum a -> Sum a -> Union Ordering

SymOrd p => SymOrd (Par1 p)

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

Methods

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

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

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

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

symCompare :: Par1 p -> Par1 p -> Union Ordering

(SymOrd a, Integral a) => SymOrd (Ratio a)

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

Methods

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

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

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

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

symCompare :: Ratio a -> Ratio a -> Union Ordering

(Generic a, GSymOrd Arity0 (Rep a), GSymEq Arity0 (Rep a)) => SymOrd (Default a)

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

Methods

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

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

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

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

symCompare :: Default a -> Default a -> Union Ordering

SymOrd a => SymOrd (Union a)

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

Methods

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

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

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

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

symCompare :: Union a -> Union a -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: IntN n -> IntN n -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: WordN n -> WordN n -> Union Ordering

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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

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

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

symCompare :: SomeBV bv -> SomeBV bv -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: SymIntN n -> SymIntN n -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: SymWordN n -> SymWordN n -> Union Ordering

SymOrd a => SymOrd (Maybe a)

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

Methods

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

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

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

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

symCompare :: Maybe a -> Maybe a -> Union Ordering

SymOrd a => SymOrd [a]

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

Methods

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

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

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

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

symCompare :: [a] -> [a] -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: Either a b -> Either a b -> Union Ordering

SymOrd (U1 p)

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

Methods

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

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

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

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

symCompare :: U1 p -> U1 p -> Union Ordering

SymOrd (V1 p)

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

Methods

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

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

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

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

symCompare :: V1 p -> V1 p -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: Default1 f a -> Default1 f a -> Union Ordering

(SymOrd a, SymOrd b) => SymOrd (CBMCEither a b)

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

Methods

(.<) :: CBMCEither a b -> CBMCEither a b -> SymBool

(.<=) :: CBMCEither a b -> CBMCEither a b -> SymBool

(.>) :: CBMCEither a b -> CBMCEither a b -> SymBool

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

symCompare :: CBMCEither a b -> CBMCEither a b -> Union Ordering

ValidFP eb sb => SymOrd (FP eb sb)

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

Methods

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

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

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

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

symCompare :: FP eb sb -> FP eb sb -> Union Ordering

ValidFP eb sb => SymOrd (SymFP eb sb)

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

Methods

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

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

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

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

symCompare :: SymFP eb sb -> SymFP eb sb -> Union Ordering

(SymOrd1 m, SymOrd a) => SymOrd (MaybeT m a)

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

Methods

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

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

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

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

symCompare :: MaybeT m a -> MaybeT m a -> Union Ordering

(SymOrd a, SymOrd b) => SymOrd (a, b)

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

Methods

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

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

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

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

symCompare :: (a, b) -> (a, b) -> Union Ordering

SymOrd a => SymOrd (Const a b)

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

Methods

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

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

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

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

symCompare :: Const a b -> Const a b -> Union Ordering

SymOrd (f a) => SymOrd (Ap f a)

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

Methods

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

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

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

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

symCompare :: Ap f a -> Ap f a -> Union Ordering

SymOrd (f a) => SymOrd (Alt f a)

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

Methods

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

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

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

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

symCompare :: Alt f a -> Alt f a -> Union Ordering

SymOrd (f p) => SymOrd (Rec1 f p)

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

Methods

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

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

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

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

symCompare :: Rec1 f p -> Rec1 f p -> Union Ordering

SymOrd (m (CBMCEither e a)) => SymOrd (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

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

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

symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> Union Ordering

(SymOrd1 m, SymOrd e, SymOrd a) => SymOrd (ExceptT e m a)

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

Methods

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

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

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

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

symCompare :: ExceptT e m a -> ExceptT e m a -> Union Ordering

(SymOrd1 m, SymOrd a) => SymOrd (IdentityT m a)

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

Methods

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

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

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

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

symCompare :: IdentityT m a -> IdentityT m a -> Union Ordering

(SymOrd1 m, SymOrd w, SymOrd a) => SymOrd (WriterT w m a)

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

Methods

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

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

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

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

symCompare :: WriterT w m a -> WriterT w m a -> Union Ordering

(SymOrd1 m, SymOrd w, SymOrd a) => SymOrd (WriterT w m a)

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

Methods

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

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

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

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

symCompare :: WriterT w m a -> WriterT w m a -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: (a, b, c) -> (a, b, c) -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: Product l r a -> Product l r a -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: Sum l r a -> Sum l r a -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: (f :*: g) p -> (f :*: g) p -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: (f :+: g) p -> (f :+: g) p -> Union Ordering

SymOrd c => SymOrd (K1 i c p)

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

Methods

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

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

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

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

symCompare :: K1 i c p -> K1 i c p -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: (a, b, c, d) -> (a, b, c, d) -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: Compose f g a -> Compose f g a -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: (f :.: g) p -> (f :.: g) p -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: M1 i c f p -> M1 i c f p -> Union Ordering

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

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

Methods

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

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

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

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

symCompare :: (a, b, c, d, e) -> (a, b, c, d, e) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, h, i) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f, g, h, i, j) -> (a, b, c, d, e, f, g, h, i, j) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f, g, h, i, j, k) -> (a, b, c, d, e, f, g, h, i, j, k) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (a, b, c, d, e, f, g, h, i, j, k, l) -> (a, b, c, d, e, f, g, h, i, j, k, l) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (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) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (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) -> Union Ordering

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

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

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

(.>) :: (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

symCompare :: (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) -> Union Ordering

class (SymEq1 f, forall a. SymOrd a => SymOrd (f a)) => SymOrd1 f where

Lifting of the SymOrd class to unary type constructors.

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

liftSymCompare symCompare should be equivalent to symCompare, under the symbolic semantics.

This class therefore represents the generalization of SymOrd 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

liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering

Lift a symCompare function through the type constructor.

The function will usually be applied to an symbolic comparison 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

SymOrd1 Identity

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Identity a -> Identity b -> Union Ordering

SymOrd1 First

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> First a -> First b -> Union Ordering

SymOrd1 Last

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Last a -> Last b -> Union Ordering

SymOrd1 Down

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Down a -> Down b -> Union Ordering

SymOrd1 Dual

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Dual a -> Dual b -> Union Ordering

SymOrd1 Product

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Product a -> Product b -> Union Ordering

SymOrd1 Sum

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Sum a -> Sum b -> Union Ordering

SymOrd1 Union

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Union a -> Union b -> Union Ordering

SymOrd1 Maybe

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Maybe a -> Maybe b -> Union Ordering

SymOrd1 List

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering

SymOrd a => SymOrd1 (Either a)

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

Methods

liftSymCompare :: (a0 -> b -> Union Ordering) -> Either a a0 -> Either a b -> Union Ordering

(Generic1 f, GSymOrd Arity1 (Rep1 f), GSymEq Arity1 (Rep1 f)) => SymOrd1 (Default1 f)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Default1 f a -> Default1 f b -> Union Ordering

SymOrd1 m => SymOrd1 (MaybeT m)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> MaybeT m a -> MaybeT m b -> Union Ordering

SymOrd a => SymOrd1 ((,) a)

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

Methods

liftSymCompare :: (a0 -> b -> Union Ordering) -> (a, a0) -> (a, b) -> Union Ordering

SymOrd a => SymOrd1 (Const a :: Type -> Type)

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

Methods

liftSymCompare :: (a0 -> b -> Union Ordering) -> Const a a0 -> Const a b -> Union Ordering

SymOrd1 f => SymOrd1 (Ap f)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Ap f a -> Ap f b -> Union Ordering

SymOrd1 f => SymOrd1 (Alt f)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Alt f a -> Alt f b -> Union Ordering

(SymOrd1 m, SymOrd e) => SymOrd1 (ExceptT e m)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> ExceptT e m a -> ExceptT e m b -> Union Ordering

SymOrd1 m => SymOrd1 (IdentityT m)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> IdentityT m a -> IdentityT m b -> Union Ordering

(SymOrd1 m, SymOrd w) => SymOrd1 (WriterT w m)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> WriterT w m a -> WriterT w m b -> Union Ordering

(SymOrd1 m, SymOrd w) => SymOrd1 (WriterT w m)

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> WriterT w m a -> WriterT w m b -> Union Ordering

(SymOrd a, SymOrd b) => SymOrd1 ((,,) a b)

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, a0) -> (a, b, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Product l r a -> Product l r b -> Union Ordering

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

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Sum l r a -> Sum l r b -> Union Ordering

(SymOrd a, SymOrd b, SymOrd c) => SymOrd1 ((,,,) a b c)

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, a0) -> (a, b, c, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a -> b -> Union Ordering) -> Compose f g a -> Compose f g b -> Union Ordering

(SymOrd a, SymOrd b, SymOrd c, SymOrd d) => SymOrd1 ((,,,,) a b c d)

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, a0) -> (a, b, c, d, b0) -> Union Ordering

(SymOrd a, SymOrd b, SymOrd c, SymOrd d, SymOrd e) => SymOrd1 ((,,,,,) a b c d e)

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, a0) -> (a, b, c, d, e, b0) -> Union Ordering

(SymOrd a, SymOrd b, SymOrd c, SymOrd d, SymOrd e, SymOrd f) => SymOrd1 ((,,,,,,) a b c d e f)

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, f, a0) -> (a, b, c, d, e, f, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, f, g, a0) -> (a, b, c, d, e, f, g, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, f, g, h, a0) -> (a, b, c, d, e, f, g, h, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, f, g, h, i, a0) -> (a, b, c, d, e, f, g, h, i, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, f, g, h, i, j, a0) -> (a, b, c, d, e, f, g, h, i, j, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (a, b, c, d, e, f, g, h, i, j, k, a0) -> (a, b, c, d, e, f, g, h, i, j, k, b0) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (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) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (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) -> Union Ordering

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

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

Methods

liftSymCompare :: (a0 -> b0 -> Union Ordering) -> (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) -> Union Ordering

symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering

Lift the standard symCompare function to binary type constructors.

class (SymEq2 f, forall a. SymOrd a => SymOrd1 (f a)) => SymOrd2 f where

Lifting of the SymOrd class to binary type constructors.

Methods

liftSymCompare2 :: (a -> b -> Union Ordering) -> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering

Lift a symCompare function through the type constructor.

The function will usually be applied to an symbolic comparison 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

SymOrd2 Either

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

Methods

liftSymCompare2 :: (a -> b -> Union Ordering) -> (c -> d -> Union Ordering) -> Either a c -> Either b d -> Union Ordering

SymOrd2 (,)

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

Methods

liftSymCompare2 :: (a -> b -> Union Ordering) -> (c -> d -> Union Ordering) -> (a, c) -> (b, d) -> Union Ordering

SymOrd a => SymOrd2 ((,,) a)

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

Methods

liftSymCompare2 :: (a0 -> b -> Union Ordering) -> (c -> d -> Union Ordering) -> (a, a0, c) -> (a, b, d) -> Union Ordering

(SymOrd a, SymOrd b) => SymOrd2 ((,,,) a b)

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

Methods

liftSymCompare2 :: (a0 -> b0 -> Union Ordering) -> (c -> d -> Union Ordering) -> (a, b, a0, c) -> (a, b, b0, d) -> Union Ordering

symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering

Lift the standard symCompare function through the type constructors.

Min and max

symMax :: (SymOrd a, ITEOp a) => a -> a -> a

Symbolic maximum.

symMin :: (SymOrd a, ITEOp a) => a -> a -> a

Symbolic minimum.

mrgMax :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a

Symbolic maximum, with a union-like monad.

mrgMin :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a

Symbolic minimum, with a union-like monad.

Generic SymOrd

data family SymOrdArgs arity a b :: Type

The arguments to the generic comparison function.

Instances

data SymOrdArgs Arity0 _ _1

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

data SymOrdArgs Arity0 _ _1 = SymOrdArgs0

newtype SymOrdArgs Arity1 a b

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

newtype SymOrdArgs Arity1 a b = SymOrdArgs1 (a -> b -> Union Ordering)

class GSymOrd arity f where

The class of types that can be generically symbolically compared.

Methods

gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering

Instances

GSymOrd Arity1 Par1

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

Methods

gsymCompare :: SymOrdArgs Arity1 a b -> Par1 a -> Par1 b -> Union Ordering

GSymOrd arity (U1 :: Type -> Type)

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

Methods

gsymCompare :: SymOrdArgs arity a b -> U1 a -> U1 b -> Union Ordering

GSymOrd arity (V1 :: Type -> Type)

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

Methods

gsymCompare :: SymOrdArgs arity a b -> V1 a -> V1 b -> Union Ordering

SymOrd1 f => GSymOrd Arity1 (Rec1 f)

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

Methods

gsymCompare :: SymOrdArgs Arity1 a b -> Rec1 f a -> Rec1 f b -> Union Ordering

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

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

Methods

gsymCompare :: SymOrdArgs arity a0 b0 -> (a :*: b) a0 -> (a :*: b) b0 -> Union Ordering

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

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

Methods

gsymCompare :: SymOrdArgs arity a0 b0 -> (a :+: b) a0 -> (a :+: b) b0 -> Union Ordering

SymOrd a => GSymOrd arity (K1 i a :: Type -> Type)

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

Methods

gsymCompare :: SymOrdArgs arity a0 b -> K1 i a a0 -> K1 i a b -> Union Ordering

(SymOrd1 f, GSymOrd Arity1 g) => GSymOrd Arity1 (f :.: g)

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

Methods

gsymCompare :: SymOrdArgs Arity1 a b -> (f :.: g) a -> (f :.: g) b -> Union Ordering

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

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

Methods

gsymCompare :: SymOrdArgs arity a0 b -> M1 i c a a0 -> M1 i c a b -> Union Ordering

genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering

Generic symCompare function.

genericLiftSymCompare :: (Generic1 f, GSymOrd Arity1 (Rep1 f)) => (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering

Generic liftSymCompare function.