Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Core.Data.Class.SubstSym

Contents

Substituting symbolic constants
Generic SubstSym

Description

Synopsis

class SubstSym a where
- substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a
class (forall a. SubstSym a => SubstSym (f a)) => SubstSym1 (f :: Type -> Type) where
- liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a
substSym1 :: forall f a cb sb (knd :: SymbolKind). (SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a -> f a
class (forall a. SubstSym a => SubstSym1 (f a)) => SubstSym2 (f :: Type -> Type -> Type) where
- liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> f a b -> f a b
substSym2 :: forall f a b cb sb (knd :: SymbolKind). (SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a b -> f a b
data family SubstSymArgs arity (knd :: SymbolKind) a cb sb
class GSubstSym arity (f :: Type -> Type) where
- gsubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a cb sb -> TypedSymbol knd cb -> sb -> f a -> f a
genericSubstSym :: forall a cb sb (knd :: SymbolKind). (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a
genericLiftSubstSym :: forall f cb sb (knd :: SymbolKind) a. (Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a

Substituting symbolic constants

class SubstSym a where Source #

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

>>> a = "a" :: TypedAnySymbol 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 :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a Source #

Instances

Instances details

SubstSym ByteString Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> ByteString -> ByteString Source #
SubstSym All Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> All -> All Source #
SubstSym Any Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Any -> Any Source #
SubstSym ArithException Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> ArithException -> ArithException Source #
SubstSym Int16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Int16 -> Int16 Source #
SubstSym Int32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Int32 -> Int32 Source #
SubstSym Int64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Int64 -> Int64 Source #
SubstSym Int8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Int8 -> Int8 Source #
SubstSym Word16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Word16 -> Word16 Source #
SubstSym Word32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Word32 -> Word32 Source #
SubstSym Word64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Word64 -> Word64 Source #
SubstSym Word8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Word8 -> Word8 Source #
SubstSym Ordering Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Ordering -> Ordering Source #
SubstSym AssertionError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> AssertionError -> AssertionError Source #
SubstSym VerificationConditions Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> VerificationConditions -> VerificationConditions Source #
SubstSym AlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> AlgReal -> AlgReal Source #
SubstSym FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> FPRoundingMode -> FPRoundingMode Source #
SubstSym NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> NotRepresentableFPError -> NotRepresentableFPError Source #
SubstSym SomeBVException Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SomeBVException -> SomeBVException Source #
SubstSym SymAlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymAlgReal -> SymAlgReal Source #
SubstSym SymBool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymBool -> SymBool Source #
SubstSym SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymFPRoundingMode -> SymFPRoundingMode Source #
SubstSym SymInteger Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymInteger -> SymInteger Source #
SubstSym Text Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Text -> Text Source #
SubstSym Integer Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Integer -> Integer Source #
SubstSym () Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> () -> () Source #
SubstSym Bool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Bool -> Bool Source #
SubstSym Char Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Char -> Char Source #
SubstSym Double Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Double -> Double Source #
SubstSym Float Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Float -> Float Source #
SubstSym Int Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Int -> Int Source #
SubstSym Word Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Word -> Word Source #
(Generic a, GSubstSym Arity0 (Rep a)) => SubstSym (Default a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Default a -> Default a Source #
SubstSym a => SubstSym (Identity a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Identity a -> Identity a Source #
SubstSym a => SubstSym (First a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> First a -> First a Source #
SubstSym a => SubstSym (Last a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Last a -> Last a Source #
SubstSym a => SubstSym (Down a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Down a -> Down a Source #
SubstSym a => SubstSym (Dual a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Dual a -> Dual a Source #
SubstSym a => SubstSym (Product a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Product a -> Product a Source #
SubstSym a => SubstSym (Sum a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Sum a -> Sum a Source #
SubstSym p => SubstSym (Par1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Par1 p -> Par1 p Source #
(Integral a, SubstSym a) => SubstSym (Ratio a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Ratio a -> Ratio a Source #
SubstSym a => SubstSym (AsKey a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> AsKey a -> AsKey a Source #
SubstSym a => SubstSym (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Union a -> Union a Source #
(KnownNat n, 1 <= n) => SubstSym (IntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => SubstSym (WordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> WordN n -> WordN n Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstSym (bv n)) => SubstSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SomeBV bv -> SomeBV bv Source #
(KnownNat n, 1 <= n) => SubstSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SubstSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymWordN n -> SymWordN n Source #
SubstSym a => SubstSym (Maybe a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Maybe a -> Maybe a Source #
SubstSym a => SubstSym [a] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> [a] -> [a] Source #
(Generic1 f, GSubstSym Arity1 (Rep1 f), SubstSym a) => SubstSym (Default1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Default1 f a -> Default1 f a Source #
(SubstSym a1, SubstSym a2) => SubstSym (Either a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Either a1 a2 -> Either a1 a2 Source #
SubstSym (Proxy a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Proxy a -> Proxy a Source #
SubstSym (U1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> U1 p -> U1 p Source #
SubstSym (V1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> V1 p -> V1 p Source #
(SubstSym1 f, SubstSym a) => SubstSym (AsKey1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> AsKey1 f a -> AsKey1 f a Source #
ValidFP eb sb => SubstSym (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> FP eb sb -> FP eb sb Source #
SubstSym (SymType b) => SubstSym (a --> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a --> b) -> a --> b Source #
ValidFP eb sb => SubstSym (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> SymFP eb sb -> SymFP eb sb Source #
SubstSym (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> (sa -~> sb) -> sa -~> sb Source #
SubstSym (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> (sa =~> sb) -> sa =~> sb Source #
(SubstSym a, SubstSym b) => SubstSym (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a =-> b) -> a =-> b Source #
(SubstSym1 a1, SubstSym a2) => SubstSym (MaybeT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> MaybeT a1 a2 -> MaybeT a1 a2 Source #
(SubstSym a1, SubstSym a2) => SubstSym (a1, a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2) -> (a1, a2) Source #
SubstSym a => SubstSym (Const a b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Const a b -> Const a b Source #
SubstSym (f a) => SubstSym (Ap f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Ap f a -> Ap f a Source #
SubstSym (f a) => SubstSym (Alt f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Alt f a -> Alt f a Source #
SubstSym (f p) => SubstSym (Rec1 f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Rec1 f p -> Rec1 f p Source #
(SubstSym a1, SubstSym1 a2, SubstSym a3) => SubstSym (ExceptT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 Source #
(SubstSym1 m, SubstSym a) => SubstSym (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> IdentityT m a -> IdentityT m a Source #
(SubstSym a1, SubstSym1 a2, SubstSym a3) => SubstSym (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> WriterT a1 a2 a3 -> WriterT a1 a2 a3 Source #
(SubstSym a1, SubstSym1 a2, SubstSym a3) => SubstSym (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> WriterT a1 a2 a3 -> WriterT a1 a2 a3 Source #
(SubstSym a1, SubstSym a2, SubstSym a3) => SubstSym (a1, a2, a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3) -> (a1, a2, a3) Source #
(SubstSym (l a), SubstSym (r a)) => SubstSym (Product l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Product l r a -> Product l r a Source #
(SubstSym (l a), SubstSym (r a)) => SubstSym (Sum l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Sum l r a -> Sum l r a Source #
(SubstSym (f p), SubstSym (g p)) => SubstSym ((f :*: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (f :: g) p -> (f :: g) p Source #
(SubstSym (f p), SubstSym (g p)) => SubstSym ((f :+: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (f :+: g) p -> (f :+: g) p Source #
SubstSym c => SubstSym (K1 i c p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> K1 i c p -> K1 i c p Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4) => SubstSym (a1, a2, a3, a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4) -> (a1, a2, a3, a4) Source #
SubstSym (f (g a)) => SubstSym (Compose f g a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> Compose f g a -> Compose f g a Source #
SubstSym (f (g p)) => SubstSym ((f :.: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (f :.: g) p -> (f :.: g) p Source #
SubstSym (f p) => SubstSym (M1 i c f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> M1 i c f p -> M1 i c f p Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5) => SubstSym (a1, a2, a3, a4, a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6) => SubstSym (a1, a2, a3, a4, a5, a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7) => SubstSym (a1, a2, a3, a4, a5, a6, a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12, SubstSym a13) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12, SubstSym a13, SubstSym a14) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12, SubstSym a13, SubstSym a14, SubstSym a15) => SubstSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #

class (forall a. SubstSym a => SubstSym (f a)) => SubstSym1 (f :: Type -> Type) where Source #

Lifting of SubstSym to unary type constructors.

Methods

liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a Source #

Lift a symbol substitution function to unary type constructors.

Instances

Instances details

SubstSym1 Identity Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Identity a -> Identity a Source #
SubstSym1 First Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> First a -> First a Source #
SubstSym1 Last Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Last a -> Last a Source #
SubstSym1 Down Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Down a -> Down a Source #
SubstSym1 Dual Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Dual a -> Dual a Source #
SubstSym1 Product Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Product a -> Product a Source #
SubstSym1 Sum Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Sum a -> Sum a Source #
SubstSym1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Union a -> Union a Source #
SubstSym1 Maybe Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Maybe a -> Maybe a Source #
SubstSym1 [] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> [a] -> [a] Source #
(Generic1 f, GSubstSym Arity1 (Rep1 f)) => SubstSym1 (Default1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Default1 f a -> Default1 f a Source #
SubstSym a => SubstSym1 (Either a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> Either a a0 -> Either a a0 Source #
SubstSym1 (Proxy :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Proxy a -> Proxy a Source #
SubstSym1 f => SubstSym1 (AsKey1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> AsKey1 f a -> AsKey1 f a Source #
SubstSym1 a => SubstSym1 (MaybeT a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> MaybeT a a0 -> MaybeT a a0 Source #
SubstSym a => SubstSym1 ((,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, a0) -> (a, a0) Source #
SubstSym a => SubstSym1 (Const a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> Const a a0 -> Const a a0 Source #
SubstSym1 f => SubstSym1 (Ap f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Ap f a -> Ap f a Source #
SubstSym1 f => SubstSym1 (Alt f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Alt f a -> Alt f a Source #
(SubstSym a1, SubstSym1 a2) => SubstSym1 (ExceptT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> ExceptT a1 a2 a -> ExceptT a1 a2 a Source #
SubstSym1 m => SubstSym1 (IdentityT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> IdentityT m a -> IdentityT m a Source #
(SubstSym a1, SubstSym1 a2) => SubstSym1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> WriterT a1 a2 a -> WriterT a1 a2 a Source #
(SubstSym a1, SubstSym1 a2) => SubstSym1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> WriterT a1 a2 a -> WriterT a1 a2 a Source #
(SubstSym a1, SubstSym a2) => SubstSym1 ((,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a) -> (a1, a2, a) Source #
(SubstSym1 l, SubstSym1 r) => SubstSym1 (Product l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Product l r a -> Product l r a Source #
(SubstSym1 l, SubstSym1 r) => SubstSym1 (Sum l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Sum l r a -> Sum l r a Source #
(SubstSym a1, SubstSym a2, SubstSym a3) => SubstSym1 ((,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a) -> (a1, a2, a3, a) Source #
(SubstSym1 f, SubstSym1 g) => SubstSym1 (Compose f g) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Compose f g a -> Compose f g a Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4) => SubstSym1 ((,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a) -> (a1, a2, a3, a4, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5) => SubstSym1 ((,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a) -> (a1, a2, a3, a4, a5, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6) => SubstSym1 ((,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a) -> (a1, a2, a3, a4, a5, a6, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7) => SubstSym1 ((,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a) -> (a1, a2, a3, a4, a5, a6, a7, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8) => SubstSym1 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9) => SubstSym1 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10) => SubstSym1 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11) => SubstSym1 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12) => SubstSym1 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12, SubstSym a13) => SubstSym1 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12, SubstSym a13, SubstSym a14) => SubstSym1 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) Source #

substSym1 :: forall f a cb sb (knd :: SymbolKind). (SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a -> f a Source #

Lifting the standard substSym to unary type constructors.

class (forall a. SubstSym a => SubstSym1 (f a)) => SubstSym2 (f :: Type -> Type -> Type) where Source #

Lifting of SubstSym to binary type constructors.

Methods

liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> f a b -> f a b Source #

Lift a symbol substitution function to binary type constructors.

Instances

Instances details

SubstSym2 Either Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> Either a b -> Either a b Source #
SubstSym2 (,) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a, b) -> (a, b) Source #
SubstSym a => SubstSym2 ((,,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a0 b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a, a0, b) -> (a, a0, b) Source #
(SubstSym a1, SubstSym a2) => SubstSym2 ((,,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a, b) -> (a1, a2, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3) => SubstSym2 ((,,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a, b) -> (a1, a2, a3, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4) => SubstSym2 ((,,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a, b) -> (a1, a2, a3, a4, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5) => SubstSym2 ((,,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a, b) -> (a1, a2, a3, a4, a5, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6) => SubstSym2 ((,,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a, b) -> (a1, a2, a3, a4, a5, a6, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7) => SubstSym2 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8) => SubstSym2 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9) => SubstSym2 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10) => SubstSym2 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11) => SubstSym2 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12) => SubstSym2 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) Source #
(SubstSym a1, SubstSym a2, SubstSym a3, SubstSym a4, SubstSym a5, SubstSym a6, SubstSym a7, SubstSym a8, SubstSym a9, SubstSym a10, SubstSym a11, SubstSym a12, SubstSym a13) => SubstSym2 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) Source #

substSym2 :: forall f a b cb sb (knd :: SymbolKind). (SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a b -> f a b Source #

Lifting the standard substSym to binary type constructors.

Generic `SubstSym`

data family SubstSymArgs arity (knd :: SymbolKind) a cb sb Source #

The arguments to the generic substSym function.

Instances

Instances details

data SubstSymArgs Arity0 _ _1 _2 _3 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym data SubstSymArgs Arity0 _ _1 _2 _3 = SubstSymArgs0
newtype SubstSymArgs Arity1 knd a cb sb Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym newtype SubstSymArgs Arity1 knd a cb sb = SubstSymArgs1 (TypedSymbol knd cb -> sb -> a -> a)

class GSubstSym arity (f :: Type -> Type) where Source #

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

Methods

gsubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a cb sb -> TypedSymbol knd cb -> sb -> f a -> f a Source #

Instances

Instances details

GSubstSym Arity1 Par1 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs Arity1 knd a cb sb -> TypedSymbol knd cb -> sb -> Par1 a -> Par1 a Source #
GSubstSym arity (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a cb sb -> TypedSymbol knd cb -> sb -> U1 a -> U1 a Source #
GSubstSym arity (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a cb sb -> TypedSymbol knd cb -> sb -> V1 a -> V1 a Source #
SubstSym1 a => GSubstSym Arity1 (Rec1 a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs Arity1 knd a0 cb sb -> TypedSymbol knd cb -> sb -> Rec1 a a0 -> Rec1 a a0 Source #
(GSubstSym arity a, GSubstSym arity b) => GSubstSym arity (a :*: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a0 cb sb -> TypedSymbol knd cb -> sb -> (a :: b) a0 -> (a :: b) a0 Source #
(GSubstSym arity a, GSubstSym arity b) => GSubstSym arity (a :+: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a0 cb sb -> TypedSymbol knd cb -> sb -> (a :+: b) a0 -> (a :+: b) a0 Source #
SubstSym a => GSubstSym arity (K1 i a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a0 cb sb -> TypedSymbol knd cb -> sb -> K1 i a a0 -> K1 i a a0 Source #
(SubstSym1 f, GSubstSym Arity1 g) => GSubstSym Arity1 (f :.: g) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs Arity1 knd a cb sb -> TypedSymbol knd cb -> sb -> (f :.: g) a -> (f :.: g) a Source #
GSubstSym arity a => GSubstSym arity (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym Methods gsubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a0 cb sb -> TypedSymbol knd cb -> sb -> M1 i c a a0 -> M1 i c a a0 Source #

genericSubstSym :: forall a cb sb (knd :: SymbolKind). (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a Source #

Generic substSym function.

genericLiftSubstSym :: forall f cb sb (knd :: SymbolKind) a. (Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a Source #

Generic liftSubstSym function.

Substituting symbolic constants

Instances

Instances

Instances

Generic SubstSym

Instances

Instances

Generic `SubstSym`