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	None
Language	Haskell2010

Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Contents

Orphan instances

Description

Orphan instances

PEvalFromIntegralTerm Integer AlgReal Source #
Instance details Methods pevalFromIntegralTerm :: Term Integer -> Term AlgReal Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType AlgReal Source #
PEvalFromIntegralTerm Integer Integer Source #
Instance details Methods pevalFromIntegralTerm :: Term Integer -> Term Integer Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType Integer Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (IntN n) Source #
Instance details Methods pevalFromIntegralTerm :: Term Integer -> Term (IntN n) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (WordN n) Source #
Instance details Methods pevalFromIntegralTerm :: Term Integer -> Term (WordN n) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (WordN n) Source #
ValidFP eb sb => PEvalFromIntegralTerm Integer (FP eb sb) Source #
Instance details Methods pevalFromIntegralTerm :: Term Integer -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal Source #
Instance details Methods pevalFromIntegralTerm :: Term (IntN n) -> Term AlgReal Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType AlgReal Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) Integer Source #
Instance details Methods pevalFromIntegralTerm :: Term (IntN n) -> Term Integer Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType Integer Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal Source #
Instance details Methods pevalFromIntegralTerm :: Term (WordN n) -> Term AlgReal Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType AlgReal Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) Integer Source #
Instance details Methods pevalFromIntegralTerm :: Term (WordN n) -> Term Integer Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType Integer Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (IntN m) Source #
Instance details Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (IntN m) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (IntN m) Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (WordN m) Source #
Instance details Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (WordN m) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (WordN m) Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (IntN m) Source #
Instance details Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (IntN m) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (IntN m) Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (WordN m) Source #
Instance details Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (WordN m) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (WordN m) Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (IntN n) (FP eb sb) Source #
Instance details Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (WordN n) (FP eb sb) Source #
Instance details Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (FP eb sb) Source #