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

Documentation

pevalGeneralLtOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #

pevalGeneralLeOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #

Orphan instances

PEvalOrdTerm Integer Source #
Instance details Methods pevalLtOrdTerm :: Term Integer -> Term Integer -> Term Bool Source # pevalLeOrdTerm :: Term Integer -> Term Integer -> Term Bool Source # withSbvOrdTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n Integer) => r) -> r Source # sbvLtOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBV Bool Source # sbvLeOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (IntN n)) => r) -> r Source # sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool Source # sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (WordN n)) => r) -> r Source # sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool Source # sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool Source #