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	Trustworthy
Language	Haskell2010

Grisette.Internal.Core.Data.Class.SOrd

Contents

Symbolic total order relation

Description

Synopsis

class SEq a => SOrd a where
- (.<) :: a -> a -> SymBool
- (.<=) :: a -> a -> SymBool
- (.>) :: a -> a -> SymBool
- (.>=) :: a -> a -> SymBool
- symCompare :: a -> a -> UnionM Ordering
class SEq' f => SOrd' f where
- (..<) :: f a -> f a -> SymBool
- (..<=) :: f a -> f a -> SymBool
- (..>) :: f a -> f a -> SymBool
- (..>=) :: f a -> f a -> SymBool
- symCompare' :: f a -> f a -> UnionM Ordering
symMax :: (SOrd a, ITEOp a) => a -> a -> a
symMin :: (SOrd a, ITEOp a) => a -> a -> a
mrgMax :: (SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) => a -> a -> m a
mrgMin :: (SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) => a -> a -> m a

Symbolic total order relation

class SEq a => SOrd a where Source #

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 UnionMBase and PlainUnion for more information.

>>> a `symCompare` b :: UnionM Ordering -- UnionM is UnionMBase specialized with SymBool
{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 SOrd via (Default X)

Minimal complete definition

(.<=)

Methods

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

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

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

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

symCompare :: a -> a -> UnionM Ordering Source #

Instances

Instances details

SOrd Int16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Int16 -> Int16 -> SymBool Source # (.<=) :: Int16 -> Int16 -> SymBool Source # (.>) :: Int16 -> Int16 -> SymBool Source # (.>=) :: Int16 -> Int16 -> SymBool Source # symCompare :: Int16 -> Int16 -> UnionM Ordering Source #
SOrd Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Int32 -> Int32 -> SymBool Source # (.<=) :: Int32 -> Int32 -> SymBool Source # (.>) :: Int32 -> Int32 -> SymBool Source # (.>=) :: Int32 -> Int32 -> SymBool Source # symCompare :: Int32 -> Int32 -> UnionM Ordering Source #
SOrd Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Int64 -> Int64 -> SymBool Source # (.<=) :: Int64 -> Int64 -> SymBool Source # (.>) :: Int64 -> Int64 -> SymBool Source # (.>=) :: Int64 -> Int64 -> SymBool Source # symCompare :: Int64 -> Int64 -> UnionM Ordering Source #
SOrd Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Int8 -> Int8 -> SymBool Source # (.<=) :: Int8 -> Int8 -> SymBool Source # (.>) :: Int8 -> Int8 -> SymBool Source # (.>=) :: Int8 -> Int8 -> SymBool Source # symCompare :: Int8 -> Int8 -> UnionM Ordering Source #
SOrd Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Word16 -> Word16 -> SymBool Source # (.<=) :: Word16 -> Word16 -> SymBool Source # (.>) :: Word16 -> Word16 -> SymBool Source # (.>=) :: Word16 -> Word16 -> SymBool Source # symCompare :: Word16 -> Word16 -> UnionM Ordering Source #
SOrd Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Word32 -> Word32 -> SymBool Source # (.<=) :: Word32 -> Word32 -> SymBool Source # (.>) :: Word32 -> Word32 -> SymBool Source # (.>=) :: Word32 -> Word32 -> SymBool Source # symCompare :: Word32 -> Word32 -> UnionM Ordering Source #
SOrd Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Word64 -> Word64 -> SymBool Source # (.<=) :: Word64 -> Word64 -> SymBool Source # (.>) :: Word64 -> Word64 -> SymBool Source # (.>=) :: Word64 -> Word64 -> SymBool Source # symCompare :: Word64 -> Word64 -> UnionM Ordering Source #
SOrd Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Word8 -> Word8 -> SymBool Source # (.<=) :: Word8 -> Word8 -> SymBool Source # (.>) :: Word8 -> Word8 -> SymBool Source # (.>=) :: Word8 -> Word8 -> SymBool Source # symCompare :: Word8 -> Word8 -> UnionM Ordering Source #
SOrd ByteString Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: ByteString -> ByteString -> SymBool Source # (.<=) :: ByteString -> ByteString -> SymBool Source # (.>) :: ByteString -> ByteString -> SymBool Source # (.>=) :: ByteString -> ByteString -> SymBool Source # symCompare :: ByteString -> ByteString -> UnionM Ordering Source #
SOrd AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: AssertionError -> AssertionError -> SymBool Source # (.<=) :: AssertionError -> AssertionError -> SymBool Source # (.>) :: AssertionError -> AssertionError -> SymBool Source # (.>=) :: AssertionError -> AssertionError -> SymBool Source # symCompare :: AssertionError -> AssertionError -> UnionM Ordering Source #
SOrd VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.<=) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.>) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.>=) :: VerificationConditions -> VerificationConditions -> SymBool Source # symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering Source #
SOrd SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymBool -> SymBool -> SymBool Source # (.<=) :: SymBool -> SymBool -> SymBool Source # (.>) :: SymBool -> SymBool -> SymBool Source # (.>=) :: SymBool -> SymBool -> SymBool Source # symCompare :: SymBool -> SymBool -> UnionM Ordering Source #
SOrd SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymInteger -> SymInteger -> SymBool Source # (.<=) :: SymInteger -> SymInteger -> SymBool Source # (.>) :: SymInteger -> SymInteger -> SymBool Source # (.>=) :: SymInteger -> SymInteger -> SymBool Source # symCompare :: SymInteger -> SymInteger -> UnionM Ordering Source #
SOrd Text Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Text -> Text -> SymBool Source # (.<=) :: Text -> Text -> SymBool Source # (.>) :: Text -> Text -> SymBool Source # (.>=) :: Text -> Text -> SymBool Source # symCompare :: Text -> Text -> UnionM Ordering Source #
SOrd Integer Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Integer -> Integer -> SymBool Source # (.<=) :: Integer -> Integer -> SymBool Source # (.>) :: Integer -> Integer -> SymBool Source # (.>=) :: Integer -> Integer -> SymBool Source # symCompare :: Integer -> Integer -> UnionM Ordering Source #
SOrd () Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: () -> () -> SymBool Source # (.<=) :: () -> () -> SymBool Source # (.>) :: () -> () -> SymBool Source # (.>=) :: () -> () -> SymBool Source # symCompare :: () -> () -> UnionM Ordering Source #
SOrd Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Bool -> Bool -> SymBool Source # (.<=) :: Bool -> Bool -> SymBool Source # (.>) :: Bool -> Bool -> SymBool Source # (.>=) :: Bool -> Bool -> SymBool Source # symCompare :: Bool -> Bool -> UnionM Ordering Source #
SOrd Char Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Char -> Char -> SymBool Source # (.<=) :: Char -> Char -> SymBool Source # (.>) :: Char -> Char -> SymBool Source # (.>=) :: Char -> Char -> SymBool Source # symCompare :: Char -> Char -> UnionM Ordering Source #
SOrd Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Int -> Int -> SymBool Source # (.<=) :: Int -> Int -> SymBool Source # (.>) :: Int -> Int -> SymBool Source # (.>=) :: Int -> Int -> SymBool Source # symCompare :: Int -> Int -> UnionM Ordering Source #
SOrd Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Word -> Word -> SymBool Source # (.<=) :: Word -> Word -> SymBool Source # (.>) :: Word -> Word -> SymBool Source # (.>=) :: Word -> Word -> SymBool Source # symCompare :: Word -> Word -> UnionM Ordering Source #
SOrd a => SOrd (Identity a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Identity a -> Identity a -> SymBool Source # (.<=) :: Identity a -> Identity a -> SymBool Source # (.>) :: Identity a -> Identity a -> SymBool Source # (.>=) :: Identity a -> Identity a -> SymBool Source # symCompare :: Identity a -> Identity a -> UnionM Ordering Source #
(SEq a, Generic a, SOrd' (Rep a)) => SOrd (Default a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Default a -> Default a -> SymBool Source # (.<=) :: Default a -> Default a -> SymBool Source # (.>) :: Default a -> Default a -> SymBool Source # (.>=) :: Default a -> Default a -> SymBool Source # symCompare :: Default a -> Default a -> UnionM Ordering Source #
(SOrd a, Mergeable a) => SOrd (UnionM a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: UnionM a -> UnionM a -> SymBool Source # (.<=) :: UnionM a -> UnionM a -> SymBool Source # (.>) :: UnionM a -> UnionM a -> SymBool Source # (.>=) :: UnionM a -> UnionM a -> SymBool Source # symCompare :: UnionM a -> UnionM a -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SOrd (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: IntN n -> IntN n -> SymBool Source # (.<=) :: IntN n -> IntN n -> SymBool Source # (.>) :: IntN n -> IntN n -> SymBool Source # (.>=) :: IntN n -> IntN n -> SymBool Source # symCompare :: IntN n -> IntN n -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SOrd (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: WordN n -> WordN n -> SymBool Source # (.<=) :: WordN n -> WordN n -> SymBool Source # (.>) :: WordN n -> WordN n -> SymBool Source # (.>=) :: WordN n -> WordN n -> SymBool Source # symCompare :: WordN n -> WordN n -> UnionM Ordering Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SOrd (bv n)) => SOrd (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.<) :: SomeBV bv -> SomeBV bv -> SymBool Source # (.<=) :: SomeBV bv -> SomeBV bv -> SymBool Source # (.>) :: SomeBV bv -> SomeBV bv -> SymBool Source # (.>=) :: SomeBV bv -> SomeBV bv -> SymBool Source # symCompare :: SomeBV bv -> SomeBV bv -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SOrd (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymIntN n -> SymIntN n -> SymBool Source # (.<=) :: SymIntN n -> SymIntN n -> SymBool Source # (.>) :: SymIntN n -> SymIntN n -> SymBool Source # (.>=) :: SymIntN n -> SymIntN n -> SymBool Source # symCompare :: SymIntN n -> SymIntN n -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SOrd (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymWordN n -> SymWordN n -> SymBool Source # (.<=) :: SymWordN n -> SymWordN n -> SymBool Source # (.>) :: SymWordN n -> SymWordN n -> SymBool Source # (.>=) :: SymWordN n -> SymWordN n -> SymBool Source # symCompare :: SymWordN n -> SymWordN n -> UnionM Ordering Source #
SOrd a => SOrd (Maybe a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Maybe a -> Maybe a -> SymBool Source # (.<=) :: Maybe a -> Maybe a -> SymBool Source # (.>) :: Maybe a -> Maybe a -> SymBool Source # (.>=) :: Maybe a -> Maybe a -> SymBool Source # symCompare :: Maybe a -> Maybe a -> UnionM Ordering Source #
SOrd a => SOrd [a] Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: [a] -> [a] -> SymBool Source # (.<=) :: [a] -> [a] -> SymBool Source # (.>) :: [a] -> [a] -> SymBool Source # (.>=) :: [a] -> [a] -> SymBool Source # symCompare :: [a] -> [a] -> UnionM Ordering Source #
(SOrd a, SOrd b) => SOrd (Either a b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Either a b -> Either a b -> SymBool Source # (.<=) :: Either a b -> Either a b -> SymBool Source # (.>) :: Either a b -> Either a b -> SymBool Source # (.>=) :: Either a b -> Either a b -> SymBool Source # symCompare :: Either a b -> Either a b -> UnionM Ordering Source #
(SOrd a, SOrd b) => SOrd (CBMCEither a b) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods (.<) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (.<=) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (.>) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (.>=) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # symCompare :: CBMCEither a b -> CBMCEither a b -> UnionM Ordering Source #
SOrd (m (Maybe a)) => SOrd (MaybeT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: MaybeT m a -> MaybeT m a -> SymBool Source # (.<=) :: MaybeT m a -> MaybeT m a -> SymBool Source # (.>) :: MaybeT m a -> MaybeT m a -> SymBool Source # (.>=) :: MaybeT m a -> MaybeT m a -> SymBool Source # symCompare :: MaybeT m a -> MaybeT m a -> UnionM Ordering Source #
(SOrd a, SOrd b) => SOrd (a, b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b) -> (a, b) -> SymBool Source # (.<=) :: (a, b) -> (a, b) -> SymBool Source # (.>) :: (a, b) -> (a, b) -> SymBool Source # (.>=) :: (a, b) -> (a, b) -> SymBool Source # symCompare :: (a, b) -> (a, b) -> UnionM Ordering Source #
SOrd (m (CBMCEither e a)) => SOrd (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 # (.>) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (.>=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> UnionM Ordering Source #
SOrd (m (Either e a)) => SOrd (ExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: ExceptT e m a -> ExceptT e m a -> SymBool Source # (.<=) :: ExceptT e m a -> ExceptT e m a -> SymBool Source # (.>) :: ExceptT e m a -> ExceptT e m a -> SymBool Source # (.>=) :: ExceptT e m a -> ExceptT e m a -> SymBool Source # symCompare :: ExceptT e m a -> ExceptT e m a -> UnionM Ordering Source #
SOrd (m a) => SOrd (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: IdentityT m a -> IdentityT m a -> SymBool Source # (.<=) :: IdentityT m a -> IdentityT m a -> SymBool Source # (.>) :: IdentityT m a -> IdentityT m a -> SymBool Source # (.>=) :: IdentityT m a -> IdentityT m a -> SymBool Source # symCompare :: IdentityT m a -> IdentityT m a -> UnionM Ordering Source #
SOrd (m (a, s)) => SOrd (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: WriterT s m a -> WriterT s m a -> SymBool Source # (.<=) :: WriterT s m a -> WriterT s m a -> SymBool Source # (.>) :: WriterT s m a -> WriterT s m a -> SymBool Source # (.>=) :: WriterT s m a -> WriterT s m a -> SymBool Source # symCompare :: WriterT s m a -> WriterT s m a -> UnionM Ordering Source #
SOrd (m (a, s)) => SOrd (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: WriterT s m a -> WriterT s m a -> SymBool Source # (.<=) :: WriterT s m a -> WriterT s m a -> SymBool Source # (.>) :: WriterT s m a -> WriterT s m a -> SymBool Source # (.>=) :: WriterT s m a -> WriterT s m a -> SymBool Source # symCompare :: WriterT s m a -> WriterT s m a -> UnionM Ordering Source #
(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b, c) -> (a, b, c) -> SymBool Source # (.<=) :: (a, b, c) -> (a, b, c) -> SymBool Source # (.>) :: (a, b, c) -> (a, b, c) -> SymBool Source # (.>=) :: (a, b, c) -> (a, b, c) -> SymBool Source # symCompare :: (a, b, c) -> (a, b, c) -> UnionM Ordering Source #
(SOrd (f a), SOrd (g a)) => SOrd (Sum f g a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: Sum f g a -> Sum f g a -> SymBool Source # (.<=) :: Sum f g a -> Sum f g a -> SymBool Source # (.>) :: Sum f g a -> Sum f g a -> SymBool Source # (.>=) :: Sum f g a -> Sum f g a -> SymBool Source # symCompare :: Sum f g a -> Sum f g a -> UnionM Ordering Source #
(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b, c, d) -> (a, b, c, d) -> SymBool Source # (.<=) :: (a, b, c, d) -> (a, b, c, d) -> SymBool Source # (.>) :: (a, b, c, d) -> (a, b, c, d) -> SymBool Source # (.>=) :: (a, b, c, d) -> (a, b, c, d) -> SymBool Source # symCompare :: (a, b, c, d) -> (a, b, c, d) -> UnionM Ordering Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool Source # (.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool Source # (.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool Source # (.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool Source # symCompare :: (a, b, c, d, e) -> (a, b, c, d, e) -> UnionM Ordering Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool Source # (.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool Source # (.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool Source # (.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool Source # symCompare :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> UnionM Ordering Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool Source # (.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool Source # (.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool Source # (.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool Source # symCompare :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> UnionM Ordering Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g, SOrd h) => SOrd (a, b, c, d, e, f, g, h) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool Source # (.<=) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool Source # (.>) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool Source # (.>=) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool Source # symCompare :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> UnionM Ordering Source #

class SEq' f => SOrd' f where Source #

Auxiliary class for SOrd instance derivation

Methods

(..<) :: f a -> f a -> SymBool infix 4 Source #

Auxiliary function for '(..<) derivation

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

Auxiliary function for '(..<=) derivation

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

Auxiliary function for '(..>) derivation

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

Auxiliary function for '(..>=) derivation

symCompare' :: f a -> f a -> UnionM Ordering Source #

Auxiliary function for symCompare derivation

Instances

Instances details

SOrd' (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (..<) :: U1 a -> U1 a -> SymBool Source # (..<=) :: U1 a -> U1 a -> SymBool Source # (..>) :: U1 a -> U1 a -> SymBool Source # (..>=) :: U1 a -> U1 a -> SymBool Source # symCompare' :: U1 a -> U1 a -> UnionM Ordering Source #
SOrd' (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (..<) :: V1 a -> V1 a -> SymBool Source # (..<=) :: V1 a -> V1 a -> SymBool Source # (..>) :: V1 a -> V1 a -> SymBool Source # (..>=) :: V1 a -> V1 a -> SymBool Source # symCompare' :: V1 a -> V1 a -> UnionM Ordering Source #
(SOrd' a, SOrd' b) => SOrd' (a :*: b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (..<) :: (a :: b) a0 -> (a :: b) a0 -> SymBool Source # (..<=) :: (a :: b) a0 -> (a :: b) a0 -> SymBool Source # (..>) :: (a :: b) a0 -> (a :: b) a0 -> SymBool Source # (..>=) :: (a :: b) a0 -> (a :: b) a0 -> SymBool Source # symCompare' :: (a :: b) a0 -> (a :: b) a0 -> UnionM Ordering Source #
(SOrd' a, SOrd' b) => SOrd' (a :+: b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (..<) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool Source # (..<=) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool Source # (..>) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool Source # (..>=) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool Source # symCompare' :: (a :+: b) a0 -> (a :+: b) a0 -> UnionM Ordering Source #
SOrd c => SOrd' (K1 i c :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (..<) :: K1 i c a -> K1 i c a -> SymBool Source # (..<=) :: K1 i c a -> K1 i c a -> SymBool Source # (..>) :: K1 i c a -> K1 i c a -> SymBool Source # (..>=) :: K1 i c a -> K1 i c a -> SymBool Source # symCompare' :: K1 i c a -> K1 i c a -> UnionM Ordering Source #
SOrd' a => SOrd' (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (..<) :: M1 i c a a0 -> M1 i c a a0 -> SymBool Source # (..<=) :: M1 i c a a0 -> M1 i c a a0 -> SymBool Source # (..>) :: M1 i c a a0 -> M1 i c a a0 -> SymBool Source # (..>=) :: M1 i c a a0 -> M1 i c a a0 -> SymBool Source # symCompare' :: M1 i c a a0 -> M1 i c a a0 -> UnionM Ordering Source #

symMax :: (SOrd a, ITEOp a) => a -> a -> a Source #

symMin :: (SOrd a, ITEOp a) => a -> a -> a Source #

mrgMax :: (SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) => a -> a -> m a Source #

mrgMin :: (SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) => a -> a -> m a Source #