Language.Hasmtlib.Orderable

Documentation

class Equatable a => Orderable a where

Compare two as as SMT-Expression.

You can derive an instance of this class if your type is Generic.

x <- var @RealSort
y <- var
assert $ x >? y
assert $ x === min' 42 100

Minimal complete definition

Nothing

Methods

(<=?) :: a -> a -> Expr BoolSort infix 4

default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort

(>=?) :: a -> a -> Expr BoolSort infix 4

(<?) :: a -> a -> Expr BoolSort infix 4

(>?) :: a -> a -> Expr BoolSort infix 4

Instances

Orderable Void

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Void -> Void -> Expr 'BoolSort

(>=?) :: Void -> Void -> Expr 'BoolSort

(<?) :: Void -> Void -> Expr 'BoolSort

(>?) :: Void -> Void -> Expr 'BoolSort

Orderable Int16

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Int16 -> Int16 -> Expr 'BoolSort

(>=?) :: Int16 -> Int16 -> Expr 'BoolSort

(<?) :: Int16 -> Int16 -> Expr 'BoolSort

(>?) :: Int16 -> Int16 -> Expr 'BoolSort

Orderable Int32

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Int32 -> Int32 -> Expr 'BoolSort

(>=?) :: Int32 -> Int32 -> Expr 'BoolSort

(<?) :: Int32 -> Int32 -> Expr 'BoolSort

(>?) :: Int32 -> Int32 -> Expr 'BoolSort

Orderable Int64

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Int64 -> Int64 -> Expr 'BoolSort

(>=?) :: Int64 -> Int64 -> Expr 'BoolSort

(<?) :: Int64 -> Int64 -> Expr 'BoolSort

(>?) :: Int64 -> Int64 -> Expr 'BoolSort

Orderable Int8

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Int8 -> Int8 -> Expr 'BoolSort

(>=?) :: Int8 -> Int8 -> Expr 'BoolSort

(<?) :: Int8 -> Int8 -> Expr 'BoolSort

(>?) :: Int8 -> Int8 -> Expr 'BoolSort

Orderable Word16

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Word16 -> Word16 -> Expr 'BoolSort

(>=?) :: Word16 -> Word16 -> Expr 'BoolSort

(<?) :: Word16 -> Word16 -> Expr 'BoolSort

(>?) :: Word16 -> Word16 -> Expr 'BoolSort

Orderable Word32

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Word32 -> Word32 -> Expr 'BoolSort

(>=?) :: Word32 -> Word32 -> Expr 'BoolSort

(<?) :: Word32 -> Word32 -> Expr 'BoolSort

(>?) :: Word32 -> Word32 -> Expr 'BoolSort

Orderable Word64

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Word64 -> Word64 -> Expr 'BoolSort

(>=?) :: Word64 -> Word64 -> Expr 'BoolSort

(<?) :: Word64 -> Word64 -> Expr 'BoolSort

(>?) :: Word64 -> Word64 -> Expr 'BoolSort

Orderable Word8

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Word8 -> Word8 -> Expr 'BoolSort

(>=?) :: Word8 -> Word8 -> Expr 'BoolSort

(<?) :: Word8 -> Word8 -> Expr 'BoolSort

(>?) :: Word8 -> Word8 -> Expr 'BoolSort

Orderable Ordering

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Ordering -> Ordering -> Expr 'BoolSort

(>=?) :: Ordering -> Ordering -> Expr 'BoolSort

(<?) :: Ordering -> Ordering -> Expr 'BoolSort

(>?) :: Ordering -> Ordering -> Expr 'BoolSort

Orderable Integer

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Integer -> Integer -> Expr 'BoolSort

(>=?) :: Integer -> Integer -> Expr 'BoolSort

(<?) :: Integer -> Integer -> Expr 'BoolSort

(>?) :: Integer -> Integer -> Expr 'BoolSort

Orderable Natural

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Natural -> Natural -> Expr 'BoolSort

(>=?) :: Natural -> Natural -> Expr 'BoolSort

(<?) :: Natural -> Natural -> Expr 'BoolSort

(>?) :: Natural -> Natural -> Expr 'BoolSort

Orderable ()

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: () -> () -> Expr 'BoolSort

(>=?) :: () -> () -> Expr 'BoolSort

(<?) :: () -> () -> Expr 'BoolSort

(>?) :: () -> () -> Expr 'BoolSort

Orderable Bool

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Bool -> Bool -> Expr 'BoolSort

(>=?) :: Bool -> Bool -> Expr 'BoolSort

(<?) :: Bool -> Bool -> Expr 'BoolSort

(>?) :: Bool -> Bool -> Expr 'BoolSort

Orderable Char

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Char -> Char -> Expr 'BoolSort

(>=?) :: Char -> Char -> Expr 'BoolSort

(<?) :: Char -> Char -> Expr 'BoolSort

(>?) :: Char -> Char -> Expr 'BoolSort

Orderable Double

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Double -> Double -> Expr 'BoolSort

(>=?) :: Double -> Double -> Expr 'BoolSort

(<?) :: Double -> Double -> Expr 'BoolSort

(>?) :: Double -> Double -> Expr 'BoolSort

Orderable Float

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Float -> Float -> Expr 'BoolSort

(>=?) :: Float -> Float -> Expr 'BoolSort

(<?) :: Float -> Float -> Expr 'BoolSort

(>?) :: Float -> Float -> Expr 'BoolSort

Orderable Int

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Int -> Int -> Expr 'BoolSort

(>=?) :: Int -> Int -> Expr 'BoolSort

(<?) :: Int -> Int -> Expr 'BoolSort

(>?) :: Int -> Int -> Expr 'BoolSort

Orderable Word

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Word -> Word -> Expr 'BoolSort

(>=?) :: Word -> Word -> Expr 'BoolSort

(<?) :: Word -> Word -> Expr 'BoolSort

(>?) :: Word -> Word -> Expr 'BoolSort

Orderable a => Orderable (Identity a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Identity a -> Identity a -> Expr 'BoolSort

(>=?) :: Identity a -> Identity a -> Expr 'BoolSort

(<?) :: Identity a -> Identity a -> Expr 'BoolSort

(>?) :: Identity a -> Identity a -> Expr 'BoolSort

Orderable a => Orderable (First a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: First a -> First a -> Expr 'BoolSort

(>=?) :: First a -> First a -> Expr 'BoolSort

(<?) :: First a -> First a -> Expr 'BoolSort

(>?) :: First a -> First a -> Expr 'BoolSort

Orderable a => Orderable (Last a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Last a -> Last a -> Expr 'BoolSort

(>=?) :: Last a -> Last a -> Expr 'BoolSort

(<?) :: Last a -> Last a -> Expr 'BoolSort

(>?) :: Last a -> Last a -> Expr 'BoolSort

Orderable a => Orderable (Dual a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Dual a -> Dual a -> Expr 'BoolSort

(>=?) :: Dual a -> Dual a -> Expr 'BoolSort

(<?) :: Dual a -> Dual a -> Expr 'BoolSort

(>?) :: Dual a -> Dual a -> Expr 'BoolSort

Orderable a => Orderable (Product a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Product a -> Product a -> Expr 'BoolSort

(>=?) :: Product a -> Product a -> Expr 'BoolSort

(<?) :: Product a -> Product a -> Expr 'BoolSort

(>?) :: Product a -> Product a -> Expr 'BoolSort

Orderable a => Orderable (Sum a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Sum a -> Sum a -> Expr 'BoolSort

(>=?) :: Sum a -> Sum a -> Expr 'BoolSort

(<?) :: Sum a -> Sum a -> Expr 'BoolSort

(>?) :: Sum a -> Sum a -> Expr 'BoolSort

Orderable a => Orderable (Tree a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Tree a -> Tree a -> Expr 'BoolSort

(>=?) :: Tree a -> Tree a -> Expr 'BoolSort

(<?) :: Tree a -> Tree a -> Expr 'BoolSort

(>?) :: Tree a -> Tree a -> Expr 'BoolSort

KnownNat n => Orderable (Expr ('BvSort n))

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

(>=?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

(<?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

(>?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

Orderable (Expr 'IntSort)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

(>=?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

(<?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

(>?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

Orderable (Expr 'RealSort)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

(>=?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

(<?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

(>?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

Orderable (Expr 'StringSort)

Lexicographic ordering for (<?) and reflexive closure of lexicographic ordering for Orderable

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort

(>=?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort

(<?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort

(>?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort

Orderable a => Orderable (Maybe a)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Maybe a -> Maybe a -> Expr 'BoolSort

(>=?) :: Maybe a -> Maybe a -> Expr 'BoolSort

(<?) :: Maybe a -> Maybe a -> Expr 'BoolSort

(>?) :: Maybe a -> Maybe a -> Expr 'BoolSort

Orderable a => Orderable [a]

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: [a] -> [a] -> Expr 'BoolSort

(>=?) :: [a] -> [a] -> Expr 'BoolSort

(<?) :: [a] -> [a] -> Expr 'BoolSort

(>?) :: [a] -> [a] -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Either a b -> Either a b -> Expr 'BoolSort

(>=?) :: Either a b -> Either a b -> Expr 'BoolSort

(<?) :: Either a b -> Either a b -> Expr 'BoolSort

(>?) :: Either a b -> Either a b -> Expr 'BoolSort

(Orderable a, Orderable b) => Orderable (a, b)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b) -> (a, b) -> Expr 'BoolSort

(>=?) :: (a, b) -> (a, b) -> Expr 'BoolSort

(<?) :: (a, b) -> (a, b) -> Expr 'BoolSort

(>?) :: (a, b) -> (a, b) -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b, c) -> (a, b, c) -> Expr 'BoolSort

(>=?) :: (a, b, c) -> (a, b, c) -> Expr 'BoolSort

(<?) :: (a, b, c) -> (a, b, c) -> Expr 'BoolSort

(>?) :: (a, b, c) -> (a, b, c) -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b, c, d) -> (a, b, c, d) -> Expr 'BoolSort

(>=?) :: (a, b, c, d) -> (a, b, c, d) -> Expr 'BoolSort

(<?) :: (a, b, c, d) -> (a, b, c, d) -> Expr 'BoolSort

(>?) :: (a, b, c, d) -> (a, b, c, d) -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b, c, d, e) -> (a, b, c, d, e) -> Expr 'BoolSort

(>=?) :: (a, b, c, d, e) -> (a, b, c, d, e) -> Expr 'BoolSort

(<?) :: (a, b, c, d, e) -> (a, b, c, d, e) -> Expr 'BoolSort

(>?) :: (a, b, c, d, e) -> (a, b, c, d, e) -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> Expr 'BoolSort

(>=?) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> Expr 'BoolSort

(<?) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> Expr 'BoolSort

(>?) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> Expr 'BoolSort

(>=?) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> Expr 'BoolSort

(<?) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> Expr 'BoolSort

(>?) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> Expr 'BoolSort

(>=?) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> Expr 'BoolSort

(<?) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> Expr 'BoolSort

(>?) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> Expr 'BoolSort

min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

Minimum of two as SMT-Expression.

max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

Maximum of two as SMT-Expression.

class GEquatable f => GOrderable f where

Methods

(<?#) :: f a -> f a -> Expr BoolSort

(<=?#) :: f a -> f a -> Expr BoolSort

Instances

GOrderable (U1 :: k -> Type)

Defined in Language.Hasmtlib.Orderable

Methods

(<?#) :: forall (a :: k0). U1 a -> U1 a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). U1 a -> U1 a -> Expr 'BoolSort

GOrderable (V1 :: k -> Type)

Defined in Language.Hasmtlib.Orderable

Methods

(<?#) :: forall (a :: k0). V1 a -> V1 a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). V1 a -> V1 a -> Expr 'BoolSort

(GOrderable f, GOrderable g) => GOrderable (f :*: g :: k -> Type)

Defined in Language.Hasmtlib.Orderable

Methods

(<?#) :: forall (a :: k0). (f :*: g) a -> (f :*: g) a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). (f :*: g) a -> (f :*: g) a -> Expr 'BoolSort

(GOrderable f, GOrderable g) => GOrderable (f :+: g :: k -> Type)

Defined in Language.Hasmtlib.Orderable

Methods

(<?#) :: forall (a :: k0). (f :+: g) a -> (f :+: g) a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). (f :+: g) a -> (f :+: g) a -> Expr 'BoolSort

Orderable a => GOrderable (K1 i a :: k -> Type)

Defined in Language.Hasmtlib.Orderable

Methods

(<?#) :: forall (a0 :: k0). K1 i a a0 -> K1 i a a0 -> Expr 'BoolSort

(<=?#) :: forall (a0 :: k0). K1 i a a0 -> K1 i a a0 -> Expr 'BoolSort

GOrderable f => GOrderable (M1 i c f :: k -> Type)

Defined in Language.Hasmtlib.Orderable

Methods

(<?#) :: forall (a :: k0). M1 i c f a -> M1 i c f a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). M1 i c f a -> M1 i c f a -> Expr 'BoolSort