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 HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.Unified.Class.UnifiedITEOp

Description

 
Synopsis

Documentation

symIte :: forall mode v. (DecideEvalMode mode, UnifiedITEOp mode v) => GetBool mode -> v -> v -> v Source #

Unified symIte operation.

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

symIte @mode (a .== b) ...
symIte (a .== b :: SymBool) ...
symIte (a .== b :: GetBool mode) ...

symIteMerge :: forall mode v. (DecideEvalMode mode, UnifiedITEOp mode v, Mergeable v) => BaseMonad mode v -> v Source #

Unified symIteMerge operation.

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

symIteMerge @mode ...
symIteMerge (... :: BaseMonad mode v) ...

class UnifiedITEOp mode v where Source #

A class that provides unified equality comparison.

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

Methods

withBaseITEOp :: (If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r Source #

Instances

Instances details
(DecideEvalMode mode, If (IsConMode mode) () (ITEOp a)) => UnifiedITEOp mode a Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedITEOp

Methods

withBaseITEOp :: (If (IsConMode mode) () (ITEOp a) => r) -> r Source #

(UnifiedITEOp 'S v, Mergeable v) => UnifiedITEOp 'S (Union v) Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedITEOp

Methods

withBaseITEOp :: (If (IsConMode 'S) () (ITEOp (Union v)) => r) -> r Source #