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

Grisette.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

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 UnionLike 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.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.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.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.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.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.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.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 ByteString Source #
Instance details Defined in Grisette.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.Core.Control.Exception 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.Core.Control.Exception Methods (<~) :: VerificationConditions -> VerificationConditions -> SymBool Source # (<=~) :: VerificationConditions -> VerificationConditions -> SymBool Source # (>~) :: VerificationConditions -> VerificationConditions -> SymBool Source # (>=~) :: VerificationConditions -> VerificationConditions -> SymBool Source # symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering Source #
SOrd Word8 Source #
Instance details Defined in Grisette.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 Integer Source #
Instance details Defined in Grisette.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.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.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.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.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.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.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.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 => SOrd (UnionM a) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM 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 #
SupportedPrim (IntN n) => SOrd (Sym (IntN n)) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (<~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source # (<=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source # (>~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source # (>=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source # symCompare :: Sym (IntN n) -> Sym (IntN n) -> UnionM Ordering Source #
SupportedPrim (WordN n) => SOrd (Sym (WordN n)) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (<~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source # (<=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source # (>~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source # (>=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source # symCompare :: Sym (WordN n) -> Sym (WordN n) -> UnionM Ordering Source #
SupportedPrim Integer => SOrd (Sym Integer) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (<~) :: Sym Integer -> Sym Integer -> SymBool Source # (<=~) :: Sym Integer -> Sym Integer -> SymBool Source # (>~) :: Sym Integer -> Sym Integer -> SymBool Source # (>=~) :: Sym Integer -> Sym Integer -> SymBool Source # symCompare :: Sym Integer -> Sym Integer -> UnionM Ordering Source #
SOrd (Sym Bool) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (<~) :: Sym Bool -> Sym Bool -> SymBool Source # (<=~) :: Sym Bool -> Sym Bool -> SymBool Source # (>~) :: Sym Bool -> Sym Bool -> SymBool Source # (>=~) :: Sym Bool -> Sym Bool -> SymBool Source # symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering Source #
SOrd a => SOrd (Maybe a) Source #
Instance details Defined in Grisette.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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 #