• 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
        • Natarr
          • Set-nat
          • Resize-nats
            • Get-nat
            • Nats-length
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Natarr

    Resize-nats

    Change the length of the natarr 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-nats$a

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