		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Rdb-test

(rdb-test bsp i) is true iff the field of i specified by bsp is nonzero.

Signature
(rdb-test bsp i) → bool
Arguments: bsp — Guard (bspp bsp).; i — Guard (integerp i).

This is analogous to Common Lisp's (ldb-test bytespec integer).

Definitions and Theorems

Function: rdb-test

(defun rdb-test (bsp i)
  (declare (xargs :guard (and (bspp bsp) (integerp i))))
  (let ((__function__ 'rdb-test))
    (declare (ignorable __function__))
    (not (eql (rdb bsp i) 0))))