• 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
  • Std/stobjs

Natarr

Abstract stobj: logically this just represents a list of |ACL2|::|NATP|s, but it is implemented as an array.

This is a simple abstract stobj array, introduced by def-1d-arr.

Definition: natarr

(defabsstobj natarr
             :foundation natarr$c
             :recognizer (natarrp :exec natarr$cp
                                  :logic natarr$ap)
             :creator (create-natarr :exec create-natarr$c
                                     :logic create-natarr$a)
             :corr-fn natarr$corr
             :exports ((nats-length :exec nats$c-length
                                    :logic nats$a-length)
                       (get-nat :exec nats$ci :logic nats$ai)
                       (set-nat :exec update-nats$ci
                                :logic update-nats$ai)
                       (resize-nats :exec resize-nats$c
                                    :logic resize-nats$a)))

Subtopics

Set-nat
Modify the nth element of the natarr array.
Resize-nats
Change the length of the natarr array.
Get-nat
Read the nth element of the natarr array.
Nats-length
Get the length of the natarr array.