• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
          • Logops-byte-functions
            • Wrb
            • Rdb
            • Bsp
            • Bspp
            • Wrb-field
            • Bsp-size
            • Bsp-position
            • Rdb-test
            • Rdb-field
            • Wrb-guard
            • Rdb-guard
          • Defword
          • Defbytetype
          • Logext
          • Logrev
          • Loghead
          • Logops-bit-functions
          • Logtail
          • Logapp
          • Logsat
          • Binary--
          • Logcdr
          • Logcar
          • Logbit
          • Logextu
          • Logcons
          • Lshu
          • Logrpl
          • Ashu
          • Logmaskp
          • Lognotu
          • Logmask
          • Imod
          • Ifloor
          • Bfix
          • Bitmaskp
          • Logite
          • Expt2
          • Zbp
          • *logops-functions*
          • Word/bit-macros
          • Logops-definitions-theory
          • Logops-functions
          • Lbfix
          • Logextu-guard
          • Lshu-guard
          • Logtail-guard
          • Logrpl-guard
          • Logrev-guard
          • Lognotu-guard
          • Logmask-guard
          • Loghead-guard
          • Logext-guard
          • Logbit-guard
          • Logapp-guard
          • Ashu-guard
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
        • Logops
      • Rtl
    • Algebra
  • Testing-utilities

• Logops-byte-functions

Rdb-field

(rdb-field bsp i) is analogous to Common Lisp's (mask-field bytespec integer).

Signature

(rdb-field bsp i) → nat

Arguments

bsp — Guard (bspp bsp).

i — Guard (integerp i).

Definitions and Theorems

Function: rdb-field

(defun rdb-field (bsp i)
  (declare (xargs :guard (and (bspp bsp) (integerp i))))
  (let ((__function__ 'rdb-field))
    (declare (ignorable __function__))
    (logand i (wrb -1 bsp 0))))