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

Contents

Orphan instances

Description

Documentation

pevalDefaultDivIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

pevalDefaultDivBoundedIntegralTerm :: (PEvalDivModIntegralTerm a, Bounded a) => Term a -> Term a -> Term a Source #

pevalDefaultModIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

pevalDefaultQuotIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

pevalDefaultQuotBoundedIntegralTerm :: (PEvalDivModIntegralTerm a, Bounded a) => Term a -> Term a -> Term a Source #

pevalDefaultRemIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

Orphan instances

PEvalDivModIntegralTerm Integer Source #
Instance details Methods pevalDivIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalModIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalQuotIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalRemIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # withSbvDivModIntegralTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (SDivisible (SBVType n Integer) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvModIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvQuotIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvRemIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source #
(KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (IntN n) Source #
Instance details Methods pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (IntN n)) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (WordN n) Source #
Instance details Methods pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (WordN n)) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #