- (.&.) : Bits a => a -> a -> a
Bitwise "and"
Totality: total
Fixity Declaration: infixl operator, level 7- (.|.) : Bits a => a -> a -> a
Bitwise "or"
Totality: total
Fixity Declaration: infixl operator, level 5- interface Bits : 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:
- 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)
- interface FiniteBits : Type -> Type
- Parameters: a
Constraints: Bits a
Methods:
- bitSize : Nat
Return the number of bits in values of type `t`.
- bitsToIndex : Subset Nat (\{arg:0} => LT arg 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 Bits64
- FiniteBits Int
- FiniteBits Int8
- FiniteBits Int16
- FiniteBits Int32
- FiniteBits Int64
- Index : Bits a => Type
- Totality: total
- bit : Bits a => Index -> a
Sets the `i`-th bit.
Totality: total- bitSize : FiniteBits a => Nat
Return the number of bits in values of type `t`.
Totality: total- bitsToIndex : FiniteBits a => Subset Nat (\{arg:0} => LT arg bitSize) -> Index
Properly correlates `bitSize` and `Index`.
Totality: total- clearBit : Bits a => a -> Index -> a
`clearBit x i` is the same as `x .&. complement (bit i)`
Totality: total- complement : Bits a => a -> a
Returns the bitwise complement of a value.
Totality: total- complementBit : Bits a => a -> Index -> a
`complementBit x i` is the same as `xor x (bit i)`.
Totality: total- fromNat : (k : Nat) -> {auto 0 _ : lt k n = True} -> Subset Nat (\{arg:0} => LT arg n)
Utility for using bitwise operations at compile
time.
```idris example
the Bits8 13 `shiftL` fromNat 3
```
Totality: total- oneBits : Bits a => a
The value with all bits set..
Totality: total- 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- setBit : Bits a => a -> Index -> a
Sets the i-th bit of a value.
Totality: total- shiftL : Bits a => a -> Index -> a
Shift the argument left by the specified number of bits.
Totality: total
Fixity Declaration: infixl operator, level 8- shiftR : Bits a => a -> Index -> a
Shift the argument right by the specified number of bits.
Totality: total
Fixity Declaration: infixl operator, level 8- testBit : Bits a => a -> Index -> Bool
Tests, whether the i-th bit is set in the given value.
Totality: total- xor : Bits a => a -> a -> a
Bitwise "xor".
Totality: total
Fixity Declaration: infixl operator, level 6- zeroBits : Bits a => a
The value with all bits unset.
Totality: total