Copyright	(c) Sirui Lu 2021-2023
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.TabularFun

Description

Synopsis

data a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
}

Documentation

data a =-> b infixr 0 Source #

Functions as a table. Use the # operator to apply the function.

>>> :set -XTypeOperators
>>> let f = TabularFun [(1, 2), (3, 4)] 0 :: Int =-> Int
>>> f # 1
2
>>> f # 2
0
>>> f # 3
4

Constructors

TabularFun
Fields funcTable :: [(a, b)] defaultFuncValue :: b

Instances

Instances details

Generic1 ((=->) a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type Rep1 ((=->) a) :: k -> Type # Methods from1 :: forall (a0 :: k). (a =-> a0) -> Rep1 ((=->) a) a0 # to1 :: forall (a0 :: k). Rep1 ((=->) a) a0 -> a =-> a0 #
(Lift a, Lift b) => Lift (a =-> b :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods lift :: Quote m => (a =-> b) -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => (a =-> b) -> Code m (a =-> b) #
NFData a => NFData1 ((=->) a) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods liftRnf :: (a0 -> ()) -> (a =-> a0) -> () #
(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 #
Generic (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type Rep (a =-> b) :: Type -> Type # Methods from :: (a =-> b) -> Rep (a =-> b) x # to :: Rep (a =-> b) x -> a =-> b #
(Show a, Show b) => Show (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods showsPrec :: Int -> (a =-> b) -> ShowS # show :: (a =-> b) -> String # showList :: [a =-> b] -> ShowS #
(NFData a, NFData b) => NFData (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods rnf :: (a =-> b) -> () #
(Eq a, Eq b) => Eq (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun 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.TabularFun Associated Types type PrimConstraint n (a =-> b) Source #
(SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Associated Types type SymType (a =-> b) Source #
(Hashable a, Hashable b) => Hashable (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods hashWithSalt :: Int -> (a =-> b) -> Int # hash :: (a =-> b) -> Int #
Eq a => Function (a =-> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods (#) :: (a =-> b) -> a -> b Source #
(SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) => PEvalApplyTerm (a =-> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun 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.SymTabularFun 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 =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb) Source # wrapTerm :: Term (ca =-> cb) -> sa =~> sb Source #
type Rep1 ((=->) a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type Rep1 ((=->) a :: Type -> Type) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (List :.: Rec1 ((,) a)) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))
type PrimConstraint n (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type PrimConstraint n (a =-> b) = (SupportedNonFuncPrim a, SupportedPrim b, PrimConstraint n b)
type SBVType n (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type SBVType n (a =-> b) = SBV (NonFuncSBVBaseType n a) -> SBVType n b
type Rep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type Rep (a =-> b) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(a, b)]) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))
type SymType (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type SymType (a =-> b) = SymType a =~> SymType b