		Search-engine friendly clone of the ACL2 documentation.

Bed-op-andc2

Function: bed-op-andc2$inline

(defun bed-op-andc2$inline nil
  (declare (xargs :guard t))
  (let ((__function__ 'bed-op-andc2))
    (declare (ignorable __function__))
    4))

Theorem: bed-op-p-of-bed-op-andc2

(defthm bed-op-p-of-bed-op-andc2
  (b* ((op (bed-op-andc2$inline)))
    (bed-op-p op))
  :rule-classes :rewrite)

Theorem: bed-op-eval-of-andc2

(defthm bed-op-eval-of-andc2
  (equal (bed-op-eval (bed-op-andc2) x y)
         (b-andc2 x y)))