grisette-0.11.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellNone
LanguageHaskell2010

Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Description

 
Synopsis

Documentation

safeAdd :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a Source #

Unified safeAdd operation.

This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:

safeAdd @mode a b

safeNeg :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> m a Source #

Unified safeNeg operation.

This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:

safeNeg @mode a

safeSub :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a Source #

Unified safeSub operation.

This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:

safeSub @mode a b

class UnifiedSafeLinearArith (mode :: EvalModeTag) e a (m :: Type -> Type) where Source #

A class that provides unified linear arithmetic operations.

We use this type class to help resolve the constraints for SafeLinearArith.

Methods

withBaseSafeLinearArith :: (SafeLinearArith e a m => r) -> r Source #

Instances

Instances details
(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S ArithException SymInteger m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode ArithException Integer m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(UnifiedBranching mode m, SafeLinearArith e a m) => UnifiedSafeLinearArith mode e a m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith e a m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymIntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymWordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith