Language.Hasmtlib.Equatable

Documentation

class Equatable a where

Test two as on equality as SMT-Expression.

    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

(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

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