• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/io
      • Std/osets
      • Std/system
      • Std/basic
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
        • Stobj-updater-independence
        • Def-1d-arr
        • Defstobj-clone
        • Def-2d-arr
        • Defabsstobj-events
        • Bitarr
          • Bits-equiv
          • Set-bit
          • Resize-bits
          • Get-bit
          • Bits-length
          • Natarr
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Bitarr

    Bits-length

    Get the length of the bitarr array.

    In the execution this just gets the array length. The logical definition is just a wrapper for len:

    Function: bits$a-length

    (defun bits$a-length (bitarr$a)
           (declare (xargs :guard (bitarr$ap bitarr$a)))
           (len bitarr$a))