Language.Hasmtlib.Equatable

Documentation

class Equatable a where

Test two as on equality as SMT-Expression.

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

    x <- var @RealType
    y <- var
    assert $ y === x && not (y /== x)

Minimal complete definition

Nothing

Methods

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

Test whether two values are equal in the SMT-Problem.

default (===) :: (Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort

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

Test whether two values are not equal in the SMT-Problem.

Instances

Equatable Void

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Int16

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Int32

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Int64

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Int8

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Word16

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Word32

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Word64

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Word8

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Ordering

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Integer

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Natural

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable ()

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Bool

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Char

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Double

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Float

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Int

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable Word

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (Identity a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (First a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (Last a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (Dual a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (Product a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (Sum a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable (Tree a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

(KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t)

Defined in Language.Hasmtlib.Equatable

Methods

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

(/==) :: Expr t -> Expr t -> Expr 'BoolSort

Equatable a => Equatable (Maybe a)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Equatable a => Equatable [a]

Defined in Language.Hasmtlib.Equatable

Methods

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

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

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

Defined in Language.Hasmtlib.Equatable

Methods

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

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

(Equatable a, Equatable b) => Equatable (a, b)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

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

Defined in Language.Hasmtlib.Equatable

Methods

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

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

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

Defined in Language.Hasmtlib.Equatable

Methods

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

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

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

Defined in Language.Hasmtlib.Equatable

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

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

Defined in Language.Hasmtlib.Equatable

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

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

Defined in Language.Hasmtlib.Equatable

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

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

Defined in Language.Hasmtlib.Equatable

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

class GEquatable f where

Methods

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

Instances

GEquatable (U1 :: k -> Type)

Defined in Language.Hasmtlib.Equatable

Methods

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

GEquatable (V1 :: k -> Type)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Defined in Language.Hasmtlib.Equatable

Methods

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

Equatable a => GEquatable (K1 i a :: k -> Type)

Defined in Language.Hasmtlib.Equatable

Methods

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

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

Defined in Language.Hasmtlib.Equatable

Methods

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