Grisette.Unified.Internal.Class.UnifiedFromIntegral

Documentation

class UnifiedFromIntegral (mode :: EvalModeTag) a b where

A class that provides unified conversion from integral types.

We use this type class to help resolve the constraints for SymFromIntegral.

Methods

withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r

Instances

UnifiedFromIntegral 'Con Integer AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral Integer, Num AlgReal) (SymFromIntegral Integer AlgReal) => r) -> r

UnifiedFromIntegral 'Con Integer Integer

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral Integer, Num Integer) (SymFromIntegral Integer Integer) => r) -> r

UnifiedFromIntegral 'Sym SymInteger SymAlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num SymAlgReal) (SymFromIntegral SymInteger SymAlgReal) => r) -> r

UnifiedFromIntegral 'Sym SymInteger SymInteger

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num SymInteger) (SymFromIntegral SymInteger SymInteger) => r) -> r

(Typeable mode, If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b)) => UnifiedFromIntegral mode a b

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con Integer (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral Integer, Num (IntN n)) (SymFromIntegral Integer (IntN n)) => r) -> r

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con Integer (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral Integer, Num (WordN n)) (SymFromIntegral Integer (WordN n)) => r) -> r

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym SymInteger (SymIntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num (SymIntN n)) (SymFromIntegral SymInteger (SymIntN n)) => r) -> r

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym SymInteger (SymWordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num (SymWordN n)) (SymFromIntegral SymInteger (SymWordN n)) => r) -> r

ValidFP eb sb => UnifiedFromIntegral 'Con Integer (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral Integer, Num (FP eb sb)) (SymFromIntegral Integer (FP eb sb)) => r) -> r

ValidFP eb sb => UnifiedFromIntegral 'Sym SymInteger (SymFP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num (SymFP eb sb)) (SymFromIntegral SymInteger (SymFP eb sb)) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (IntN n') AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (IntN n'), Num AlgReal) (SymFromIntegral (IntN n') AlgReal) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (IntN n') Integer

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (IntN n'), Num Integer) (SymFromIntegral (IntN n') Integer) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (WordN n') AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (WordN n'), Num AlgReal) (SymFromIntegral (WordN n') AlgReal) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (WordN n') Integer

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (WordN n'), Num Integer) (SymFromIntegral (WordN n') Integer) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Sym (SymIntN n') SymAlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymIntN n'), Num SymAlgReal) (SymFromIntegral (SymIntN n') SymAlgReal) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Sym (SymIntN n') SymInteger

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymIntN n'), Num SymInteger) (SymFromIntegral (SymIntN n') SymInteger) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Sym (SymWordN n') SymAlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymWordN n'), Num SymAlgReal) (SymFromIntegral (SymWordN n') SymAlgReal) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Sym (SymWordN n') SymInteger

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymWordN n'), Num SymInteger) (SymFromIntegral (SymWordN n') SymInteger) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (IntN n') (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (IntN n'), Num (IntN n)) (SymFromIntegral (IntN n') (IntN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (IntN n') (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (IntN n'), Num (WordN n)) (SymFromIntegral (IntN n') (WordN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (WordN n') (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (WordN n'), Num (IntN n)) (SymFromIntegral (WordN n') (IntN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (WordN n') (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (WordN n'), Num (WordN n)) (SymFromIntegral (WordN n') (WordN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym (SymIntN n') (SymIntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymIntN n'), Num (SymIntN n)) (SymFromIntegral (SymIntN n') (SymIntN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym (SymIntN n') (SymWordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymIntN n'), Num (SymWordN n)) (SymFromIntegral (SymIntN n') (SymWordN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym (SymWordN n') (SymIntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymWordN n'), Num (SymIntN n)) (SymFromIntegral (SymWordN n') (SymIntN n)) => r) -> r

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym (SymWordN n') (SymWordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymWordN n'), Num (SymWordN n)) (SymFromIntegral (SymWordN n') (SymWordN n)) => r) -> r

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'Con (IntN n') (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (IntN n'), Num (FP eb sb)) (SymFromIntegral (IntN n') (FP eb sb)) => r) -> r

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'Con (WordN n') (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Con) (Integral (WordN n'), Num (FP eb sb)) (SymFromIntegral (WordN n') (FP eb sb)) => r) -> r

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'Sym (SymIntN n') (SymFP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymIntN n'), Num (SymFP eb sb)) (SymFromIntegral (SymIntN n') (SymFP eb sb)) => r) -> r

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'Sym (SymWordN n') (SymFP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymWordN n'), Num (SymFP eb sb)) (SymFromIntegral (SymWordN n') (SymFP eb sb)) => r) -> r

symFromIntegral :: forall mode a b. (Typeable mode, UnifiedFromIntegral mode a b) => a -> b

Unified symFromIntegral operation.

This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:

symFromIntegral @mode a