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.Unified.BVBVConversion

Description

Synopsis

class (UnifiedBVBVConversionImpl mode (GetWordN mode) (GetWordN mode) n0 n1 (GetWordN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetWordN mode) (GetIntN mode) n0 n1 (GetWordN mode n0) (GetIntN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetWordN mode) n0 n1 (GetIntN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetIntN mode) n0 n1 (GetIntN mode n0) (GetIntN mode n1)) => UnifiedBVBVConversion (mode :: EvalModeTag) (n0 :: Nat) (n1 :: Nat)
class (forall (n0 :: Nat) (n1 :: Nat). (KnownNat n0, KnownNat n1, 1 <= n0, 1 <= n1) => UnifiedBVBVConversion mode n0 n1) => AllUnifiedBVBVConversion (mode :: EvalModeTag)

Documentation

class (UnifiedBVBVConversionImpl mode (GetWordN mode) (GetWordN mode) n0 n1 (GetWordN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetWordN mode) (GetIntN mode) n0 n1 (GetWordN mode n0) (GetIntN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetWordN mode) n0 n1 (GetIntN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetIntN mode) n0 n1 (GetIntN mode n0) (GetIntN mode n1)) => UnifiedBVBVConversion (mode :: EvalModeTag) (n0 :: Nat) (n1 :: Nat) Source #

Unified constraints for conversion between bit-vectors.

Instances details

(UnifiedBVBVConversionImpl mode (GetWordN mode) (GetWordN mode) n0 n1 (GetWordN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetWordN mode) (GetIntN mode) n0 n1 (GetWordN mode n0) (GetIntN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetWordN mode) n0 n1 (GetIntN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetIntN mode) n0 n1 (GetIntN mode n0) (GetIntN mode n1)) => UnifiedBVBVConversion mode n0 n1 Source #

Instance details

class (forall (n0 :: Nat) (n1 :: Nat). (KnownNat n0, KnownNat n1, 1 <= n0, 1 <= n1) => UnifiedBVBVConversion mode n0 n1) => AllUnifiedBVBVConversion (mode :: EvalModeTag) Source #

Evaluation mode with unified conversion from bit-vectors to bit-vectors.

Instances details

(forall (n0 :: Nat) (n1 :: Nat). (KnownNat n0, KnownNat n1, 1 <= n0, 1 <= n1) => UnifiedBVBVConversion mode n0 n1) => AllUnifiedBVBVConversion mode Source #
Instance details Defined in Grisette.Internal.Unified.BVBVConversion