• 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

Resize-bits

Change the length of the bitarr array.

In the execution this resizes (to grow or shrink) the underlying Common Lisp array. The logical definition is based on resize-list:

Function: resize-bits$a

(defun resize-bits$a (stobjs::i bitarr$a)
       (declare (xargs :guard (bitarr$ap bitarr$a)))
       (resize-list bitarr$a stobjs::i '0))