• 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
    • 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.