• 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

    Nats-length

    Get the length of the natarr array.

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

    Function: nats$a-length

    (defun nats$a-length (natarr$a)
           (declare (xargs :guard (natarr$ap natarr$a)))
           (len natarr$a))