Language.Hasmtlib.Orderable

Documentation

class Equatable a => Orderable a where

Compare two as as SMT-Expression.

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

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

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