		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Mk-const-prop

Signature
(mk-const-prop op left right) → bed
Arguments: op — Operator being applied to these operands.
Guard (bed-op-p op).; left — First argument to the operator (a terminal bed).
Guard (atom left).; right — Second argument to the operator (a terminal bed).
Guard (atom right).

Definitions and Theorems

Function: mk-const-prop

(defun mk-const-prop (op left right)
  (declare (xargs :guard (and (bed-op-p op)
                              (atom left)
                              (atom right))))
  (let ((__function__ 'mk-const-prop))
    (declare (ignorable __function__))
    (if (mbt (and (atom left) (atom right)))
        (eql 1
             (bed-op-eval op (bool->bit left)
                          (bool->bit right)))
      (mk-op-raw op left right))))

Theorem: bed-eval-of-mk-const-prop

(defthm bed-eval-of-mk-const-prop
  (equal (bed-eval (mk-const-prop op left right)
                   env)
         (bed-eval (mk-op-raw op left right)
                   env)))