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.PEvalNumTerm

Contents

Orphan instances

Description

Documentation

pevalDefaultAddNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #

pevalDefaultNegNumTerm :: PEvalNumTerm a => Term a -> Term a Source #

Orphan instances

PEvalNumTerm Integer Source #
Instance details Methods pevalAddNumTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalNegNumTerm :: Term Integer -> Term Integer Source # pevalMulNumTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalAbsNumTerm :: Term Integer -> Term Integer Source # pevalSignumNumTerm :: Term Integer -> Term Integer Source # withSbvNumTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Num (SBVType n Integer) => r) -> r Source # sbvAddNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvNegNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer Source # sbvMulNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvAbsNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer Source # sbvSignumNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (IntN n) Source #
Instance details Methods pevalAddNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalNegNumTerm :: Term (IntN n) -> Term (IntN n) Source # pevalMulNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalAbsNumTerm :: Term (IntN n) -> Term (IntN n) Source # pevalSignumNumTerm :: Term (IntN n) -> Term (IntN n) Source # withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (IntN n)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (WordN n) Source #
Instance details Methods pevalAddNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalNegNumTerm :: Term (WordN n) -> Term (WordN n) Source # pevalMulNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalAbsNumTerm :: Term (WordN n) -> Term (WordN n) Source # pevalSignumNumTerm :: Term (WordN n) -> Term (WordN n) Source # withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (WordN n)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
ValidFP eb sb => PEvalNumTerm (FP eb sb) Source #
Instance details Methods pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # withSbvNumTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Num (SBVType n (FP eb sb)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvNegNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvMulNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvAbsNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvSignumNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #