		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Mk-op-raw

Raw construct for an binary operator node.

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

Definitions and Theorems

Function: mk-op-raw$inline

(defun mk-op-raw$inline (op left right)
  (declare (xargs :guard (bed-op-p op)))
  (let ((__function__ 'mk-op-raw))
    (declare (ignorable __function__))
    (hons (hons left right)
          (mbe :logic (bed-op-fix op) :exec op))))

Theorem: bed-eval-of-mk-op-raw

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