		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Wrb-guard

(wrb-guard i bsp j) is a macro form of the guards for wrb and wrb-field.

Macro: wrb-guard

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