• 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

Get-nat

Read the nth element of the natarr array.

In the execution this is an array access, but the logical definition is just a thin wrapper for nth:

Function: nats$ai

(defun
   nats$ai (stobjs::i natarr$a)
   (declare
        (xargs :guard (and (natarr$ap natarr$a)
                           (integerp stobjs::i)
                           (<= 0 stobjs::i)
                           (< stobjs::i (nats$a-length natarr$a)))))
   (ec-call (nfix (ec-call (nth stobjs::i natarr$a)))))