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

Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Contents

Orphan instances

Description

Synopsis

pevalGeneralLtOrdTerm :: (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm :: (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool

Documentation

pevalGeneralLtOrdTerm :: (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool Source #

General partially evaluation of less than operation.

pevalGeneralLeOrdTerm :: (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool Source #

General partially evaluation of less than or equal to operation.

Orphan instances

PEvalOrdTerm AlgReal Source #
Instance details Methods pevalLtOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source # pevalLeOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType AlgReal) => r) -> r Source # sbvLtOrdTerm :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source # sbvLeOrdTerm :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source #
PEvalOrdTerm FPRoundingMode Source #
Instance details Methods pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType FPRoundingMode) => r) -> r Source # sbvLtOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source # sbvLeOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #
PEvalOrdTerm Integer Source #
Instance details Methods pevalLtOrdTerm :: Term Integer -> Term Integer -> Term Bool Source # pevalLeOrdTerm :: Term Integer -> Term Integer -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType Integer) => r) -> r Source # sbvLtOrdTerm :: SBVType Integer -> SBVType Integer -> SBV Bool Source # sbvLeOrdTerm :: SBVType Integer -> SBVType Integer -> SBV Bool Source #
(KnownNat n, 1 <= n) => PEvalOrdTerm (IntN n) Source #
Instance details Methods pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source # pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (IntN n)) => r) -> r Source # sbvLtOrdTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBV Bool Source #
(KnownNat n, 1 <= n) => PEvalOrdTerm (WordN n) Source #
Instance details Methods pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source # pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (WordN n)) => r) -> r Source # sbvLtOrdTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBV Bool Source #
ValidFP eb sb => PEvalOrdTerm (FP eb sb) Source #
Instance details Methods pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (FP eb sb)) => r) -> r Source # sbvLtOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #