Data.Bits

Reexports

Definitions

interface Bits : Type -> Type

  The `Bits` interface defines bitwise operations over integral types.

Parameters: a
Methods:

0 Index : Type

(.&.) : a -> a -> a

  Bitwise "and"

Fixity Declaration: infixl operator, level 7

(.|.) : a -> a -> a

  Bitwise "or"

Fixity Declaration: infixl operator, level 5

xor : a -> a -> a

  Bitwise "xor".

Fixity Declaration: infixl operator, level 6

shiftL : a -> Index -> a

  Shift the argument left by the specified number of bits.

Fixity Declaration: infixl operator, level 8

shiftR : a -> Index -> a

  Shift the argument right by the specified number of bits.

Fixity Declaration: infixl operator, level 8

bit : Index -> a

  Sets the `i`-th bit.

zeroBits : a

  The value with all bits unset.

complement : a -> a

  Returns the bitwise complement of a value.

oneBits : a

  The value with all bits set..

complementBit : a -> Index -> a

  `complementBit x i` is the same as `xor x (bit i)`.

clearBit : a -> Index -> a

  `clearBit x i` is the same as `x .&. complement (bit i)`

testBit : a -> Index -> Bool

  Tests, whether the i-th bit is set in the given value.

setBit : a -> Index -> a

  Sets the i-th bit of a value.

Implementations:

Bits a => Bits (Identity a)

Bits Bits8

Bits Bits16

Bits Bits32

Bits Bits64

Bits Int

Bits Int8

Bits Int16

Bits Int32

Bits Int64

Bits Integer

Bits a => Bits (Const a b)

0 Index : Bits a => Type

Totality: total
Visibility: public export

(.&.) : Bits a => a -> a -> a

  Bitwise "and"

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

(.|.) : Bits a => a -> a -> a

  Bitwise "or"

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

xor : Bits a => a -> a -> a

  Bitwise "xor".

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 6

shiftL : {auto __con : Bits a} -> a -> Index -> a

  Shift the argument left by the specified number of bits.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

shiftR : {auto __con : Bits a} -> a -> Index -> a

  Shift the argument right by the specified number of bits.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

bit : {auto __con : Bits a} -> Index -> a

  Sets the `i`-th bit.

Totality: total
Visibility: public export

zeroBits : Bits a => a

  The value with all bits unset.

Totality: total
Visibility: public export

complement : Bits a => a -> a

  Returns the bitwise complement of a value.

Totality: total
Visibility: public export

oneBits : Bits a => a

  The value with all bits set..

Totality: total
Visibility: public export

complementBit : {auto __con : Bits a} -> a -> Index -> a

  `complementBit x i` is the same as `xor x (bit i)`.

Totality: total
Visibility: public export

clearBit : {auto __con : Bits a} -> a -> Index -> a

  `clearBit x i` is the same as `x .&. complement (bit i)`

Totality: total
Visibility: public export

testBit : {auto __con : Bits a} -> a -> Index -> Bool

  Tests, whether the i-th bit is set in the given value.

Totality: total
Visibility: public export

setBit : {auto __con : Bits a} -> a -> Index -> a

  Sets the i-th bit of a value.

Totality: total
Visibility: public export

interface FiniteBits : Type -> Type

Parameters: a
Constraints: Bits a
Methods:

bitSize : Nat

  Return the number of bits in values of type `t`.

bitsToIndex : Fin bitSize -> Index

  Properly correlates `bitSize` and `Index`.

popCount : a -> Nat

  Return the number of set bits in the argument.  This number is
  known as the population count or the Hamming weight.

rotR : a -> Fin bitSize -> a

  Rotate the argument right by the specified number of bits.

rotL : a -> Fin bitSize -> a

  Rotate the argument left by the specified number of bits.

Implementations:

FiniteBits Bits8

FiniteBits Bits16

FiniteBits Bits32

FiniteBits Bits64

FiniteBits Int

FiniteBits Int8

FiniteBits Int16

FiniteBits Int32

FiniteBits Int64

bitSize : FiniteBits a => Nat

  Return the number of bits in values of type `t`.

Totality: total
Visibility: public export

bitsToIndex : {auto __con : FiniteBits a} -> Fin bitSize -> Index

  Properly correlates `bitSize` and `Index`.

Totality: total
Visibility: public export

popCount : FiniteBits a => a -> Nat

  Return the number of set bits in the argument.  This number is
  known as the population count or the Hamming weight.

Totality: total
Visibility: public export

rotR : {auto __con : FiniteBits a} -> a -> Fin bitSize -> a

  Rotate the argument right by the specified number of bits.

Totality: total
Visibility: public export

rotL : {auto __con : FiniteBits a} -> a -> Fin bitSize -> a

  Rotate the argument left by the specified number of bits.

Totality: total
Visibility: public export

asBitVector : {auto {conArg:6938} : FiniteBits a} -> a -> Vect bitSize Bool

Totality: total
Visibility: public export

asString : FiniteBits a => a -> String

Totality: total
Visibility: public export