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

Description

 
Synopsis

Documentation

class UnifiedSymEq (mode :: EvalModeTag) a where Source #

A class that provides unified equality comparison.

We use this type class to help resolve the constraints for Eq and SymEq.

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r Source #

Instances

Instances details
DecideEvalMode mode => UnifiedSymEq mode ByteString Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq ByteString) (SymEq ByteString) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Int16 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Int16) (SymEq Int16) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Int32 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Int32) (SymEq Int32) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Int64 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Int64) (SymEq Int64) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Int8 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Int8) (SymEq Int8) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Word16 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Word16) (SymEq Word16) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Word32 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Word32) (SymEq Word32) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Word64 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Word64) (SymEq Word64) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Word8 Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Word8) (SymEq Word8) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode AssertionError Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq AssertionError) (SymEq AssertionError) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode VerificationConditions Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq VerificationConditions) (SymEq VerificationConditions) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode FPRoundingMode Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq FPRoundingMode) (SymEq FPRoundingMode) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Text Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Text) (SymEq Text) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Integer Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Integer) (SymEq Integer) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode () Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq ()) (SymEq ()) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Bool Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Bool) (SymEq Bool) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Char Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Char) (SymEq Char) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Double Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Double) (SymEq Double) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Float Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Float) (SymEq Float) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Int Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Int) (SymEq Int) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode Word Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq Word) (SymEq Word) => r) -> r Source #

(DecideEvalMode mode, If (IsConMode mode) (Eq a) (SymEq a)) => UnifiedSymEq mode a Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r Source #

UnifiedSymEq 'S v => UnifiedSymEq 'S (Union v) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode 'S) (Eq (Union v)) (SymEq (Union v)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq mode (Identity a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (Identity a)) (SymEq (Identity a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq mode (Ratio a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (Ratio a)) (SymEq (Ratio a)) => r) -> r Source #

(DecideEvalMode mode, KnownNat a, 1 <= a) => UnifiedSymEq mode (IntN a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (IntN a)) (SymEq (IntN a)) => r) -> r Source #

(DecideEvalMode mode, KnownNat a, 1 <= a) => UnifiedSymEq mode (WordN a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (WordN a)) (SymEq (WordN a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq mode (Maybe a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (Maybe a)) (SymEq (Maybe a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq mode [a] Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq [a]) (SymEq [a]) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2) => UnifiedSymEq mode (Either a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (Either a1 a2)) (SymEq (Either a1 a2)) => r) -> r Source #

(DecideEvalMode mode, ValidFP a1 a2) => UnifiedSymEq mode (FP a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (FP a1 a2)) (SymEq (FP a1 a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq1 mode a1, UnifiedSymEq mode a2) => UnifiedSymEq mode (MaybeT a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (MaybeT a1 a2)) (SymEq (MaybeT a1 a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2) => UnifiedSymEq mode (a1, a2) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2)) (SymEq (a1, a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq1 mode a2, UnifiedSymEq mode a3) => UnifiedSymEq mode (ExceptT a1 a2 a3) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (ExceptT a1 a2 a3)) (SymEq (ExceptT a1 a2 a3)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq1 mode m, UnifiedSymEq mode a) => UnifiedSymEq mode (IdentityT m a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq1 mode a2, UnifiedSymEq mode a3) => UnifiedSymEq mode (WriterT a1 a2 a3) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (WriterT a1 a2 a3)) (SymEq (WriterT a1 a2 a3)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq1 mode a2, UnifiedSymEq mode a3) => UnifiedSymEq mode (WriterT a1 a2 a3) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (WriterT a1 a2 a3)) (SymEq (WriterT a1 a2 a3)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3) => UnifiedSymEq mode (a1, a2, a3) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3)) (SymEq (a1, a2, a3)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq1 mode f, UnifiedSymEq1 mode g, UnifiedSymEq mode a) => UnifiedSymEq mode (Sum f g a) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4) => UnifiedSymEq mode (a1, a2, a3, a4) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4)) (SymEq (a1, a2, a3, a4)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5) => UnifiedSymEq mode (a1, a2, a3, a4, a5) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5)) (SymEq (a1, a2, a3, a4, a5)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6)) (SymEq (a1, a2, a3, a4, a5, a6)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7)) (SymEq (a1, a2, a3, a4, a5, a6, a7)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9, UnifiedSymEq mode a10) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9, UnifiedSymEq mode a10, UnifiedSymEq mode a11) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9, UnifiedSymEq mode a10, UnifiedSymEq mode a11, UnifiedSymEq mode a12) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9, UnifiedSymEq mode a10, UnifiedSymEq mode a11, UnifiedSymEq mode a12, UnifiedSymEq mode a13) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9, UnifiedSymEq mode a10, UnifiedSymEq mode a11, UnifiedSymEq mode a12, UnifiedSymEq mode a13, UnifiedSymEq mode a14) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3, UnifiedSymEq mode a4, UnifiedSymEq mode a5, UnifiedSymEq mode a6, UnifiedSymEq mode a7, UnifiedSymEq mode a8, UnifiedSymEq mode a9, UnifiedSymEq mode a10, UnifiedSymEq mode a11, UnifiedSymEq mode a12, UnifiedSymEq mode a13, UnifiedSymEq mode a14, UnifiedSymEq mode a15) => UnifiedSymEq mode (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source # 
Instance details

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

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)) (SymEq (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)) => r) -> r Source #

class (forall a. UnifiedSymEq mode a => UnifiedSymEq mode (f a)) => UnifiedSymEq1 (mode :: EvalModeTag) (f :: Type -> Type) where Source #

A class that provides unified lifting of equality comparison.

We use this type class to help resolve the constraints for Eq1 and SymEq1.

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r Source #

Instances

Instances details
DecideEvalMode mode => UnifiedSymEq1 mode Identity Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 Identity) (SymEq1 Identity) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq1 mode Maybe Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 Maybe) (SymEq1 Maybe) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq1 mode [] Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 []) (SymEq1 []) => r) -> r Source #

(DecideEvalMode mode, If (IsConMode mode) (Eq1 f) (SymEq1 f), forall a. UnifiedSymEq mode a => UnifiedSymEq mode (f a)) => UnifiedSymEq1 mode f Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq1 mode (Either a) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (Either a)) (SymEq1 (Either a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq1 mode a) => UnifiedSymEq1 mode (MaybeT a) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (MaybeT a)) (SymEq1 (MaybeT a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq1 mode ((,) a) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 ((,) a)) (SymEq1 ((,) a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq1 mode a2) => UnifiedSymEq1 mode (ExceptT a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (ExceptT a1 a2)) (SymEq1 (ExceptT a1 a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq1 mode m) => UnifiedSymEq1 mode (IdentityT m) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq1 mode a2) => UnifiedSymEq1 mode (WriterT a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (WriterT a1 a2)) (SymEq1 (WriterT a1 a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq1 mode a2) => UnifiedSymEq1 mode (WriterT a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (WriterT a1 a2)) (SymEq1 (WriterT a1 a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2) => UnifiedSymEq1 mode ((,,) a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 ((,,) a1 a2)) (SymEq1 ((,,) a1 a2)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq1 mode f, UnifiedSymEq1 mode g) => UnifiedSymEq1 mode (Sum f g) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2, UnifiedSymEq mode a3) => UnifiedSymEq1 mode ((,,,) a1 a2 a3) Source # 
Instance details

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

Methods

withBaseSymEq1 :: (If (IsConMode mode) (Eq1 ((,,,) a1 a2 a3)) (SymEq1 ((,,,) a1 a2 a3)) => r) -> r Source #

class (forall a. UnifiedSymEq mode a => UnifiedSymEq1 mode (f a)) => UnifiedSymEq2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where Source #

A class that provides unified lifting of equality comparison.

We use this type class to help resolve the constraints for Eq2 and SymEq2.

Methods

withBaseSymEq2 :: (If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r Source #

Instances

Instances details
DecideEvalMode mode => UnifiedSymEq2 mode Either Source # 
Instance details

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

Methods

withBaseSymEq2 :: (If (IsConMode mode) (Eq2 Either) (SymEq2 Either) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq2 mode (,) Source # 
Instance details

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

Methods

withBaseSymEq2 :: (If (IsConMode mode) (Eq2 (,)) (SymEq2 (,)) => r) -> r Source #

(DecideEvalMode mode, If (IsConMode mode) (Eq2 f) (SymEq2 f), forall a. UnifiedSymEq mode a => UnifiedSymEq1 mode (f a)) => UnifiedSymEq2 mode f Source # 
Instance details

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

Methods

withBaseSymEq2 :: (If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq2 mode ((,,) a) Source # 
Instance details

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

Methods

withBaseSymEq2 :: (If (IsConMode mode) (Eq2 ((,,) a)) (SymEq2 ((,,) a)) => r) -> r Source #

(DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2) => UnifiedSymEq2 mode ((,,,) a1 a2) Source # 
Instance details

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

Methods

withBaseSymEq2 :: (If (IsConMode mode) (Eq2 ((,,,) a1 a2)) (SymEq2 ((,,,) a1 a2)) => r) -> r Source #

(.==) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode Source #

Unified (.==).

Note that you may sometimes need to write type annotations for the result when the mode isn't clear:

a .== b :: GetBool mode

One example when it isn't clear is when this is used in unified mrgIf.

(./=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode Source #

Unified (./=).

Note that you may sometimes need to write type annotations for the result when the mode isn't clear:

a ./= b :: GetBool mode

One example when it isn't clear is when this is used in unified mrgIf.

symDistinct :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => [a] -> GetBool mode Source #

Unified symDistinct.

Note that you may sometimes need to write type annotations for the result when the mode isn't clear:

symDistinct l :: GetBool mode

One example when it isn't clear is when this is used in unified mrgIf.

liftSymEq :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymEq1 mode f) => (a -> b -> GetBool mode) -> f a -> f b -> GetBool mode Source #

Unified liftSymEq.

symEq1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) => f a -> f a -> GetBool mode Source #

Unified symEq1.

liftSymEq2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymEq2 mode f) => (a -> b -> GetBool mode) -> (c -> d -> GetBool mode) -> f a c -> f b d -> GetBool mode Source #

Unified liftSymEq2.

symEq2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq mode b, UnifiedSymEq2 mode f) => f a b -> f a b -> GetBool mode Source #

Unified symEq2.