Copyright	(c) Sirui Lu 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.SymPrim.GeneralFun

Description

Synopsis

data a --> b where
- GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
buildGeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b

Documentation

data a --> b where infixr 0 Source #

General symbolic function type. Use the # operator to apply the function. Note that this function should be applied to symbolic values only. It is by itself already a symbolic value, but can be considered partially concrete as the function body is specified. Use -~> for uninterpreted general symbolic functions.

The result would be partially evaluated.

>>> :set -XOverloadedStrings
>>> :set -XTypeOperators
>>> let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
>>> f # 1    -- 1 has the type SymInteger
(+ 2 y)
>>> f # "a"  -- "a" has the type SymInteger
(+ 1 (+ a y))

Constructors

GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b

Instances

Instances details

Lift (a --> b :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods lift :: Quote m => (a --> b) -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => (a --> b) -> Code m (a --> b) #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM (ca --> cb) -> sa -~> sb Source #
Show (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods showsPrec :: Int -> (a --> b) -> ShowS # show :: (a --> b) -> String # showList :: [a --> b] -> ShowS #
NFData (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods rnf :: (a --> b) -> () #
Eq (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods (==) :: (a --> b) -> (a --> b) -> Bool # (/=) :: (a --> b) -> (a --> b) -> Bool #
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type SBVType n (a --> b) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))) Source # pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> g))))))) Source # pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> g))))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> g)))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> g))))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a --> (b --> (c --> (d --> (e --> f))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> f)))))) Source # pformatCon :: (a --> (b --> (c --> (d --> (e --> f))))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> (e --> f)))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> f))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> f))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> f))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> f)))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a --> (b --> (c --> (d --> e)))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> e))))) Source # pformatCon :: (a --> (b --> (c --> (d --> e)))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> e))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> e)))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> e))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> e)))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> e))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> e))))), Typeable (SBVType n (a --> (b --> (c --> (d --> e)))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> e))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a --> (b --> (c --> d))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> d)))) Source # pformatCon :: (a --> (b --> (c --> d))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> d))) -> String Source # defaultValue :: a --> (b --> (c --> d)) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> d))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) Source # pevalEqTerm :: Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> d))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> d)))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> d))), SMTDefinable (SBVType n (a --> (b --> (c --> d)))), Mergeable (SBVType n (a --> (b --> (c --> d)))), Typeable (SBVType n (a --> (b --> (c --> d))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> d)) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a --> (b --> c)) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> c))) Source # pformatCon :: (a --> (b --> c)) -> String Source # pformatSym :: TypedSymbol (a --> (b --> c)) -> String Source # defaultValue :: a --> (b --> c) Source # defaultValueDynamic :: proxy (a --> (b --> c)) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term (a --> (b --> c)) Source # pevalEqTerm :: Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> c)) -> SBVType n (a --> (b --> c)) Source # symSBVName :: TypedSymbol (a --> (b --> c)) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> c))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> c)), SMTDefinable (SBVType n (a --> (b --> c))), Mergeable (SBVType n (a --> (b --> c))), Typeable (SBVType n (a --> (b --> c)))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> c) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> b)) Source # pformatCon :: (a --> b) -> String Source # pformatSym :: TypedSymbol (a --> b) -> String Source # defaultValue :: a --> b Source # defaultValueDynamic :: proxy (a --> b) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> b) -> Term (a --> b) -> Term (a --> b) Source # pevalEqTerm :: Term (a --> b) -> Term (a --> b) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> b) -> SBVType n (a --> b) Source # symSBVName :: TypedSymbol (a --> b) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> b)) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> b), SMTDefinable (SBVType n (a --> b)), Mergeable (SBVType n (a --> b)), Typeable (SBVType n (a --> b))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBVType n (a --> b) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> b Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type PrimConstraint n (a --> b) Source #
(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Associated Types type SymType (ca --> cb) Source #
Hashable (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods hashWithSalt :: Int -> (a --> b) -> Int # hash :: (a --> b) -> Int #
(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods (#) :: (a --> b) -> sa -> sb Source #
(SupportedPrim (a --> b), SupportedNonFuncPrim a, SupportedPrim b) => PEvalApplyTerm (a --> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods pevalApplyTerm :: Term (a --> b) -> Term a -> Term b Source # sbvApplyTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n a -> SBVType n b Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods con :: (ca --> cb) -> sa -~> sb Source # conView :: (sa -~> sb) -> Maybe (ca --> cb) Source # sym :: Symbol -> sa -~> sb Source # ssym :: Identifier -> sa -~> sb Source # isym :: Identifier -> Int -> sa -~> sb Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: (sa -~> sb) -> Maybe (ca --> cb) Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (ca --> cb) -> sa -~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods underlyingTerm :: (sa -~> sb) -> Term (ca --> cb) Source # wrapTerm :: Term (ca --> cb) -> sa -~> sb Source #
type PrimConstraint n (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun type PrimConstraint n (a --> b) = (SupportedNonFuncPrim a, SupportedPrim b, PrimConstraint n b, SBVType n (a --> b) ~ (SBV (NonFuncSBVBaseType n a) -> SBVType n b))
type SBVType n (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun type SBVType n (a --> b) = SBV (NonFuncSBVBaseType n a) -> SBVType n b
type SymType (ca --> cb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun type SymType (ca --> cb) = SymType ca -~> SymType cb

buildGeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b Source #

substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b Source #