Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Language.Hasmtlib.Internal.Bitvec
Synopsis
- newtype Bitvec (n :: Nat) = Bitvec {}
- bvReverse :: Bitvec n -> Bitvec n
- bvReplicate :: forall n. KnownNat n => Bit -> Bitvec n
- bvReplicate' :: forall n proxy. KnownNat n => proxy n -> Bit -> Bitvec n
- bvGenerate :: forall n. KnownNat n => (Finite n -> Bit) -> Bitvec n
- bvConcat :: Bitvec n -> Bitvec m -> Bitvec (n + m)
- bvTake' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> Bitvec n
- bvDrop' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> Bitvec m
- bvSplitAt' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> (Bitvec n, Bitvec m)
- bvToList :: Bitvec n -> [Bit]
- bvFromListN :: forall n. KnownNat n => [Bit] -> Maybe (Bitvec n)
- bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n)
- bvRotL :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n
- bvRotR :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n
- bvShL :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
- bvLShR :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
- bvZeroExtend :: KnownNat i => Proxy i -> Bitvec n -> Bitvec (n + i)
- bvExtract :: forall n i j. (KnownNat i, KnownNat ((j - i) + 1), (i + (n - i)) ~ n, (((j - i) + 1) + ((n - i) - ((j - i) + 1))) ~ (n - i)) => Proxy i -> Proxy j -> Bitvec n -> Bitvec ((j - i) + 1)
Documentation
newtype Bitvec (n :: Nat) Source #
Unsigned and length-indexed bitvector with MSB first.
Instances
KnownNat n => Bounded (Bitvec n) Source # | |
KnownNat n => Enum (Bitvec n) Source # | |
Defined in Language.Hasmtlib.Internal.Bitvec | |
KnownNat n => Num (Bitvec n) Source # | |
Defined in Language.Hasmtlib.Internal.Bitvec | |
KnownNat n => Integral (Bitvec n) Source # | |
Defined in Language.Hasmtlib.Internal.Bitvec | |
KnownNat n => Real (Bitvec n) Source # | |
Defined in Language.Hasmtlib.Internal.Bitvec Methods toRational :: Bitvec n -> Rational # | |
Show (Bitvec n) Source # | |
Eq (Bitvec n) Source # | |
Ord (Bitvec n) Source # | |
Defined in Language.Hasmtlib.Internal.Bitvec | |
KnownNat n => Boolean (Bitvec n) Source # | |
Defined in Language.Hasmtlib.Internal.Bitvec Methods bool :: Bool -> Bitvec n Source # (&&) :: Bitvec n -> Bitvec n -> Bitvec n Source # (||) :: Bitvec n -> Bitvec n -> Bitvec n Source # (==>) :: Bitvec n -> Bitvec n -> Bitvec n Source # (<==) :: Bitvec n -> Bitvec n -> Bitvec n Source # (<==>) :: Bitvec n -> Bitvec n -> Bitvec n Source # | |
Render (Bitvec n) Source # | |