Hoogle Search
Within LTS Haskell 24.28 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
(
.=== ) :: EqSymbolic a => a -> a -> SBoolsbv Data.SBV.Internals Strong equality. On floats (SFloat/SDouble), strong equality is object equality; that is NaN == NaN holds, but +0 == -0 doesn't. On other types, (.===) is simply (.==). Note that (.==) is the right notion of equality for floats per IEEE754 specs, since by definition +0 == -0 and NaN equals no other value including itself. But occasionally we want to be stronger and state NaN equals NaN and +0 and -0 are different from each other. In a context where your type is concrete, simply use fpIsEqualObject. But in a polymorphic context, use the strong equality instead. NB. If you do not care about or work with floats, simply use (.==) and (./=).
(
.=> ) :: SBool -> SBool -> SBoolsbv Data.SBV.Internals Symbolic implication
(
.|| ) :: SBool -> SBool -> SBoolsbv Data.SBV.Internals Symbolic disjunction
(
.~& ) :: SBool -> SBool -> SBoolsbv Data.SBV.Internals Symbolic nand
(
.~| ) :: SBool -> SBool -> SBoolsbv Data.SBV.Internals Symbolic nor
(
.: ) :: SymVal a => SBV a -> SList a -> SList asbv Data.SBV.List Prepend an element, the traditional cons.
(
.% ) :: SInteger -> SInteger -> SRationalsbv Data.SBV.Rational Construct a symbolic rational from a given numerator and denominator. Note that it is not possible to deconstruct a rational by taking numerator and denominator fields, since we do not represent them canonically. (This is due to the fact that SMTLib has no functions to compute the GCD. One can use the maximization engine to compute the GCD of numbers, but not as a function.)
(
.: ) :: SChar -> SString -> SStringsbv Data.SBV.String Prepend an element, the traditional cons.
(
.&& ) :: SBool -> SBool -> SBoolsbv Data.SBV.Trans Symbolic conjunction
(
./= ) :: EqSymbolic a => a -> a -> SBoolsbv Data.SBV.Trans Symbolic inequality.