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