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
Bits : Type -> Type
The `Bits` interface defines bitwise operations over integral types.
Parameters: a
Methods:
Index : Type
(.&.) : a -> a -> a
Bitwise "and"
(.|.) : a -> a -> a
Bitwise "or"
xor : a -> a -> a
Bitwise "xor".
shiftL : a -> Index -> a
Shift the argument left by the specified number of bits.
shiftR : a -> Index -> a
Shift the argument right by the specified number of bits.
bit : (i : 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 : (x : a) -> (i : Index) -> a
`complementBit x i` is the same as `xor x (bit i)`.
clearBit : (x : a) -> (i : 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 -> (i : Index) -> a
Sets the i-th bit of a value.

Implementations:
Bitsa => Bits (Identitya)
Bits Bits8
Bits Bits16
Bits Bits32
Bits Int
Bitsa => Bits (Constab)
FiniteBits : Type -> Type
Parameters: a
Constraints: Bits a
Methods:
bitSize : Nat
Return the number of bits in values of type `t`.
bitsToIndex : SubsetNat (\{arg:0} => LT{arg:0}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.

Implementations:
FiniteBits Bits8
FiniteBits Bits16
FiniteBits Bits32
FiniteBits Int
Index : Bitsa => Type
Totality: total
bit : {auto __con : 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 : {auto __con : FiniteBitsa} -> SubsetNat (\{arg:0} => LT{arg:0}bitSize) -> Index
Properly correlates `bitSize` and `Index`.
Totality: total
clearBit : {auto __con : 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 : {auto __con : 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} => LT{arg:0}n)
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 : {auto __con : Bitsa} -> a -> Index -> a
Sets the i-th bit of a value.
Totality: total
shiftL : {auto __con : Bitsa} -> a -> Index -> a
Shift the argument left by the specified number of bits.
Totality: total
Fixity Declaration: infixl operator, level 8
shiftR : {auto __con : Bitsa} -> a -> Index -> a
Shift the argument right by the specified number of bits.
Totality: total
Fixity Declaration: infixl operator, level 8
testBit : {auto __con : 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