Idris2Doc : Data.Bits

Data.Bits

(.&.) : Bitsa => a -> a -> a
  Bitwise "and"

Totality: total
Fixity Declaration: infixl operator, level 7
(.|.) : Bitsa => a -> a -> a
  Bitwise "or"

Totality: total
Fixity Declaration: infixl operator, level 5
interfaceBits : Type -> Type
  The `Bits` interface defines bitwise operations over integral types.

Parameters: a
Methods:
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:
Bitsa => Bits (Identitya)
BitsBits8
BitsBits16
BitsBits32
BitsBits64
BitsInt
BitsInt8
BitsInt16
BitsInt32
BitsInt64
BitsInteger
Bitsa => Bits (Constab)
interfaceFiniteBits : Type -> Type
Parameters: a
Constraints: Bits a
Methods:
bitSize : Nat
  Return the number of bits in values of type `t`.
bitsToIndex : SubsetNat (\{arg:0} => LTargbitSize) -> 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.

Implementations:
FiniteBitsBits8
FiniteBitsBits16
FiniteBitsBits32
FiniteBitsBits64
FiniteBitsInt
FiniteBitsInt8
FiniteBitsInt16
FiniteBitsInt32
FiniteBitsInt64
Index : Bitsa => Type
Totality: total
bit : Bitsa => Index -> a
  Sets the `i`-th bit.

Totality: total
bitSize : FiniteBitsa => Nat
  Return the number of bits in values of type `t`.

Totality: total
bitsToIndex : FiniteBitsa => SubsetNat (\{arg:0} => LTargbitSize) -> Index
  Properly correlates `bitSize` and `Index`.

Totality: total
clearBit : Bitsa => a -> Index -> a
  `clearBit x i` is the same as `x .&. complement (bit i)`

Totality: total
complement : Bitsa => a -> a
  Returns the bitwise complement of a value.

Totality: total
complementBit : Bitsa => a -> Index -> a
  `complementBit x i` is the same as `xor x (bit i)`.

Totality: total
fromNat : (k : Nat) -> {auto 0 _ : ltkn = True} -> SubsetNat (\{arg:0} => LTargn)
  Utility for using bitwise operations at compile
time.

```idris example
the Bits8 13 `shiftL` fromNat 3
```

Totality: total
oneBits : Bitsa => a
  The value with all bits set..

Totality: total
popCount : FiniteBitsa => 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
setBit : Bitsa => a -> Index -> a
  Sets the i-th bit of a value.

Totality: total
shiftL : Bitsa => a -> Index -> a
  Shift the argument left by the specified number of bits.

Totality: total
Fixity Declaration: infixl operator, level 8
shiftR : Bitsa => a -> Index -> a
  Shift the argument right by the specified number of bits.

Totality: total
Fixity Declaration: infixl operator, level 8
testBit : Bitsa => a -> Index -> Bool
  Tests, whether the i-th bit is set in the given value.

Totality: total
xor : Bitsa => a -> a -> a
  Bitwise "xor".

Totality: total
Fixity Declaration: infixl operator, level 6
zeroBits : Bitsa => a
  The value with all bits unset.

Totality: total