Grisette.Internal.Core.Data.Class.SubstSym

Substituting symbolic constants

class SubstSym a where

Substitution of symbols (symbolic constants) to a symbolic value.

>>> a = "a" :: TypedSymbol Bool
>>> v = "x" .&& "y" :: SymBool
>>> substSym a v (["a" .&& "b", "a"] :: [SymBool])
[(&& (&& x y) b),(&& x y)]

Note 1: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extensions.

data X = ... deriving Generic deriving SubstSym via (Default X)

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a

Instances

SubstSym All

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> All -> All

SubstSym Any

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Any -> Any

SubstSym Int16

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int16 -> Int16

SubstSym Int32

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int32 -> Int32

SubstSym Int64

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int64 -> Int64

SubstSym Int8

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int8 -> Int8

SubstSym Word16

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word16 -> Word16

SubstSym Word32

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word32 -> Word32

SubstSym Word64

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word64 -> Word64

SubstSym Word8

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word8 -> Word8

SubstSym ByteString

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> ByteString -> ByteString

SubstSym Ordering

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Ordering -> Ordering

SubstSym AssertionError

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> AssertionError -> AssertionError

SubstSym VerificationConditions

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> VerificationConditions -> VerificationConditions

SubstSym FPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> FPRoundingMode -> FPRoundingMode

SubstSym SymBool

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymBool -> SymBool

SubstSym SymFPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymFPRoundingMode -> SymFPRoundingMode

SubstSym SymInteger

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymInteger -> SymInteger

SubstSym Text

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Text -> Text

SubstSym Integer

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Integer -> Integer

SubstSym ()

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> () -> ()

SubstSym Bool

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Bool -> Bool

SubstSym Char

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Char -> Char

SubstSym Double

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Double -> Double

SubstSym Float

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Float -> Float

SubstSym Int

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int -> Int

SubstSym Word

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word -> Word

SubstSym a => SubstSym (Identity a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Identity a -> Identity a

SubstSym a => SubstSym (First a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> First a -> First a

SubstSym a => SubstSym (Last a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Last a -> Last a

SubstSym a => SubstSym (Down a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Down a -> Down a

SubstSym a => SubstSym (Dual a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Dual a -> Dual a

SubstSym a => SubstSym (Product a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Product a -> Product a

SubstSym a => SubstSym (Sum a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Sum a -> Sum a

SubstSym p => SubstSym (Par1 p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Par1 p -> Par1 p

(Generic a, GSubstSym Arity0 (Rep a)) => SubstSym (Default a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Default a -> Default a

SubstSym a => SubstSym (Union a)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Union a -> Union a

(KnownNat n, 1 <= n) => SubstSym (IntN n)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n

(KnownNat n, 1 <= n) => SubstSym (WordN n)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n

(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstSym (bv n)) => SubstSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv

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

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymWordN n -> SymWordN n

SubstSym a => SubstSym (Maybe a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Maybe a -> Maybe a

SubstSym a => SubstSym [a]

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> [a] -> [a]

(SubstSym a, SubstSym b) => SubstSym (Either a b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Either a b -> Either a b

SubstSym (U1 p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> U1 p -> U1 p

SubstSym (V1 p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> V1 p -> V1 p

(Generic1 f, GSubstSym Arity1 (Rep1 f), SubstSym a) => SubstSym (Default1 f a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Default1 f a -> Default1 f a

ValidFP eb sb => SubstSym (FP eb sb)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> FP eb sb -> FP eb sb

ValidFP eb sb => SubstSym (SymFP eb sb)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> SymFP eb sb -> SymFP eb sb

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

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa -~> sb) -> sa -~> sb

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

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa =~> sb) -> sa =~> sb

(SubstSym1 m, SubstSym a) => SubstSym (MaybeT m a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a

(SubstSym a, SubstSym b) => SubstSym (a, b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b) -> (a, b)

SubstSym a => SubstSym (Const a b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Const a b -> Const a b

SubstSym (f a) => SubstSym (Ap f a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Ap f a -> Ap f a

SubstSym (f a) => SubstSym (Alt f a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Alt f a -> Alt f a

SubstSym (f p) => SubstSym (Rec1 f p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Rec1 f p -> Rec1 f p

(SubstSym1 m, SubstSym e, SubstSym a) => SubstSym (ExceptT e m a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a

(SubstSym1 m, SubstSym a) => SubstSym (IdentityT m a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a

(SubstSym1 m, SubstSym a, SubstSym s) => SubstSym (WriterT s m a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a

(SubstSym1 m, SubstSym a, SubstSym s) => SubstSym (WriterT s m a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a

(SubstSym a, SubstSym b, SubstSym c) => SubstSym (a, b, c)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c) -> (a, b, c)

(SubstSym (l a), SubstSym (r a)) => SubstSym (Product l r a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Product l r a -> Product l r a

(SubstSym (l a), SubstSym (r a)) => SubstSym (Sum l r a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Sum l r a -> Sum l r a

(SubstSym (f p), SubstSym (g p)) => SubstSym ((f :*: g) p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (f :*: g) p -> (f :*: g) p

(SubstSym (f p), SubstSym (g p)) => SubstSym ((f :+: g) p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (f :+: g) p -> (f :+: g) p

SubstSym c => SubstSym (K1 i c p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> K1 i c p -> K1 i c p

(SubstSym a, SubstSym b, SubstSym c, SubstSym d) => SubstSym (a, b, c, d)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d) -> (a, b, c, d)

SubstSym (f (g a)) => SubstSym (Compose f g a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Compose f g a -> Compose f g a

SubstSym (f (g p)) => SubstSym ((f :.: g) p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (f :.: g) p -> (f :.: g) p

SubstSym (f p) => SubstSym (M1 i c f p)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> M1 i c f p -> M1 i c f p

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e) => SubstSym (a, b, c, d, e)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e) -> (a, b, c, d, e)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f) => SubstSym (a, b, c, d, e, f)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g) => SubstSym (a, b, c, d, e, f, g)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h) => SubstSym (a, b, c, d, e, f, g, h)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i) => SubstSym (a, b, c, d, e, f, g, h, i)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, h, i)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j) => SubstSym (a, b, c, d, e, f, g, h, i, j)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j) -> (a, b, c, d, e, f, g, h, i, j)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k) => SubstSym (a, b, c, d, e, f, g, h, i, j, k)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k) -> (a, b, c, d, e, f, g, h, i, j, k)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l) => SubstSym (a, b, c, d, e, f, g, h, i, j, k, l)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l) -> (a, b, c, d, e, f, g, h, i, j, k, l)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m) => SubstSym (a, b, c, d, e, f, g, h, i, j, k, l, m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m) -> (a, b, c, d, e, f, g, h, i, j, k, l, m)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m, SubstSym n) => SubstSym (a, b, c, d, e, f, g, h, i, j, k, l, m, n)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m, SubstSym n, SubstSym o) => SubstSym (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)

class (forall a. SubstSym a => SubstSym (f a)) => SubstSym1 f where

Lifting of SubstSym to unary type constructors.

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> f a -> f a

Lift a symbol substitution function to unary type constructors.

Instances

SubstSym1 Identity

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Identity a -> Identity a

SubstSym1 First

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> First a -> First a

SubstSym1 Last

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Last a -> Last a

SubstSym1 Down

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Down a -> Down a

SubstSym1 Dual

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Dual a -> Dual a

SubstSym1 Product

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Product a -> Product a

SubstSym1 Sum

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Sum a -> Sum a

SubstSym1 Union

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Union a -> Union a

SubstSym1 Maybe

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Maybe a -> Maybe a

SubstSym1 List

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> [a] -> [a]

SubstSym a => SubstSym1 (Either a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> Either a a0 -> Either a a0

(Generic1 f, GSubstSym Arity1 (Rep1 f)) => SubstSym1 (Default1 f)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Default1 f a -> Default1 f a

SubstSym1 m => SubstSym1 (MaybeT m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a

SubstSym a => SubstSym1 ((,) a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, a0) -> (a, a0)

SubstSym a => SubstSym1 (Const a :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> Const a a0 -> Const a a0

SubstSym1 f => SubstSym1 (Ap f)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Ap f a -> Ap f a

SubstSym1 f => SubstSym1 (Alt f)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Alt f a -> Alt f a

(SubstSym1 m, SubstSym e) => SubstSym1 (ExceptT e m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a

SubstSym1 m => SubstSym1 (IdentityT m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a

(SubstSym1 m, SubstSym s) => SubstSym1 (WriterT s m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a

(SubstSym1 m, SubstSym s) => SubstSym1 (WriterT s m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a

(SubstSym a, SubstSym b) => SubstSym1 ((,,) a b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, a0) -> (a, b, a0)

(SubstSym1 l, SubstSym1 r) => SubstSym1 (Product l r)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Product l r a -> Product l r a

(SubstSym1 l, SubstSym1 r) => SubstSym1 (Sum l r)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Sum l r a -> Sum l r a

(SubstSym a, SubstSym b, SubstSym c) => SubstSym1 ((,,,) a b c)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, a0) -> (a, b, c, a0)

(SubstSym1 f, SubstSym1 g) => SubstSym1 (Compose f g)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> Compose f g a -> Compose f g a

(SubstSym a, SubstSym b, SubstSym c, SubstSym d) => SubstSym1 ((,,,,) a b c d)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, a0) -> (a, b, c, d, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e) => SubstSym1 ((,,,,,) a b c d e)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, a0) -> (a, b, c, d, e, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f) => SubstSym1 ((,,,,,,) a b c d e f)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, a0) -> (a, b, c, d, e, f, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g) => SubstSym1 ((,,,,,,,) a b c d e f g)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, a0) -> (a, b, c, d, e, f, g, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h) => SubstSym1 ((,,,,,,,,) a b c d e f g h)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, a0) -> (a, b, c, d, e, f, g, h, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i) => SubstSym1 ((,,,,,,,,,) a b c d e f g h i)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, a0) -> (a, b, c, d, e, f, g, h, i, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j) => SubstSym1 ((,,,,,,,,,,) a b c d e f g h i j)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, a0) -> (a, b, c, d, e, f, g, h, i, j, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k) => SubstSym1 ((,,,,,,,,,,,) a b c d e f g h i j k)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, a0) -> (a, b, c, d, e, f, g, h, i, j, k, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l) => SubstSym1 ((,,,,,,,,,,,,) a b c d e f g h i j k l)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m) => SubstSym1 ((,,,,,,,,,,,,,) a b c d e f g h i j k l m)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0)

(SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m, SubstSym n) => SubstSym1 ((,,,,,,,,,,,,,,) a b c d e f g h i j k l m n)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0)

substSym1 :: (SubstSym1 f, SubstSym a, LinkedRep cb sb) => TypedSymbol cb -> sb -> f a -> f a

Lifting the standard substSym to unary type constructors.

class (forall a. SubstSym a => SubstSym1 (f a)) => SubstSym2 f where

Lifting of SubstSym to binary type constructors.

Methods

liftSubstSym2 :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> (TypedSymbol cb -> sb -> b -> b) -> TypedSymbol cb -> sb -> f a b -> f a b

Lift a symbol substitution function to binary type constructors.

Instances

SubstSym2 Either

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym2 :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> (TypedSymbol cb -> sb -> b -> b) -> TypedSymbol cb -> sb -> Either a b -> Either a b

SubstSym2 (,)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym2 :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a -> a) -> (TypedSymbol cb -> sb -> b -> b) -> TypedSymbol cb -> sb -> (a, b) -> (a, b)

SubstSym a => SubstSym2 ((,,) a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym2 :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> (TypedSymbol cb -> sb -> b -> b) -> TypedSymbol cb -> sb -> (a, a0, b) -> (a, a0, b)

(SubstSym a, SubstSym b) => SubstSym2 ((,,,) a b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

liftSubstSym2 :: LinkedRep cb sb => (TypedSymbol cb -> sb -> a0 -> a0) -> (TypedSymbol cb -> sb -> b0 -> b0) -> TypedSymbol cb -> sb -> (a, b, a0, b0) -> (a, b, a0, b0)

substSym2 :: (SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb) => TypedSymbol cb -> sb -> f a b -> f a b

Lifting the standard substSym to binary type constructors.

Generic SubstSym

data family SubstSymArgs arity a cb sb :: Type

The arguments to the generic substSym function.

Instances

data SubstSymArgs Arity0 _ _1 _2

Defined in Grisette.Internal.Core.Data.Class.SubstSym

data SubstSymArgs Arity0 _ _1 _2 = SubstSymArgs0

newtype SubstSymArgs Arity1 a cb sb

Defined in Grisette.Internal.Core.Data.Class.SubstSym

newtype SubstSymArgs Arity1 a cb sb = SubstSymArgs1 (TypedSymbol cb -> sb -> a -> a)

class GSubstSym arity f where

The class of types where we can generically substitute the symbols in a value.

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a

Instances

GSubstSym Arity1 Par1

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs Arity1 a cb sb -> TypedSymbol cb -> sb -> Par1 a -> Par1 a

GSubstSym arity (U1 :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> U1 a -> U1 a

GSubstSym arity (V1 :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> V1 a -> V1 a

SubstSym1 a => GSubstSym Arity1 (Rec1 a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs Arity1 a0 cb sb -> TypedSymbol cb -> sb -> Rec1 a a0 -> Rec1 a a0

(GSubstSym arity a, GSubstSym arity b) => GSubstSym arity (a :*: b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a0 cb sb -> TypedSymbol cb -> sb -> (a :*: b) a0 -> (a :*: b) a0

(GSubstSym arity a, GSubstSym arity b) => GSubstSym arity (a :+: b)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a0 cb sb -> TypedSymbol cb -> sb -> (a :+: b) a0 -> (a :+: b) a0

SubstSym a => GSubstSym arity (K1 i a :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a0 cb sb -> TypedSymbol cb -> sb -> K1 i a a0 -> K1 i a a0

(SubstSym1 f, GSubstSym Arity1 g) => GSubstSym Arity1 (f :.: g)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs Arity1 a cb sb -> TypedSymbol cb -> sb -> (f :.: g) a -> (f :.: g) a

GSubstSym arity a => GSubstSym arity (M1 i c a)

Defined in Grisette.Internal.Core.Data.Class.SubstSym

Methods

gsubstSym :: LinkedRep cb sb => SubstSymArgs arity a0 cb sb -> TypedSymbol cb -> sb -> M1 i c a a0 -> M1 i c a a0

genericSubstSym :: (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb) => TypedSymbol cb -> sb -> a -> a

Generic substSym function.

genericLiftSubstSym :: (Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb) => (TypedSymbol cb -> sb -> a -> a) -> TypedSymbol cb -> sb -> f a -> f a

Generic liftSubstSym function.