Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Std/lists
Std/alists
Obags
Std/util
Std/strings
Std/io
Std/osets
Std/basic
Std/system
Std/typed-lists
Std/bitsets
Bitsets
Bitset-members
Bitset-insert
Bitset-delete
Bitset-intersectp
Bitset-intersect
Bitset-difference
Bitset-subsetp
Bitset-union
Bitset-memberp
Bitset-singleton
Bitset-list
Bitset-cardinality
Bitset-list*
Utilities
Bits-between
Bits-0-31
60bits-0-59
Add-to-each
Bits-0-7
60bits-0-7
60bits-0-3
Sbitsets
Reasoning
Std/testing
Std/typed-alists
Std/stobjs
Std-extensions
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Bitsets
Utilities
Utility functions.
Subtopics
Bits-between
(bits-between n m x)
returns a proper, ordered set of all
i
in
[n, m)
such that
(
logbitp
i x)
.
Bits-0-31
60bits-0-59
Partially unrolled version of
bits-between
that collects the bits from a 60-bit unsigned
x
and adds
offset
to each.
Add-to-each
Add an offset to each member of a list.
Bits-0-7
Inner loop for
bits-0-31
.
60bits-0-7
Identical to
bits-0-7
, but for 60-bit unsigned ints.
60bits-0-3
Like
bits-0-7
, but since 8 doesn't divide 60, we have this goofy function for the final bits.