• 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-guard

    (rdb-guard bsp i) is a macro form of the guards for rdb, rdb-test, and rdb-field.

    Macro: rdb-guard

    (defmacro rdb-guard (bsp i)
      (cons 'and
            (cons (cons 'force
                        (cons (cons 'bspp (cons bsp 'nil))
                              'nil))
                  (cons (cons 'force
                              (cons (cons 'integerp (cons i 'nil))
                                    'nil))
                        'nil))))