Grisette.Core.Data.Class.ITEOp

Documentation

class ITEOp v where

ITE operator for solvable (see Grisette.Core)s, including symbolic boolean, integer, etc.

>>> let a = "a" :: SymBool
>>> let b = "b" :: SymBool
>>> let c = "c" :: SymBool
>>> symIte a b c
(ite a b c)

Methods

symIte :: SymBool -> v -> v -> v

Instances

ITEOp SomeSymIntN

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN

ITEOp SomeSymWordN

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN

ITEOp SymBool

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymBool -> SymBool -> SymBool

ITEOp SymInteger

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger

(ITEOp a, Mergeable a) => ITEOp (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

symIte :: SymBool -> UnionM a -> UnionM a -> UnionM a

(KnownNat n, 1 <= n) => ITEOp (SymIntN n)

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => ITEOp (SymWordN n)

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa -~> sb)

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb)

Defined in Grisette.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb