		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Mk-var-raw

Raw constructor for a variable ITE node.

Signature
(mk-var-raw var left right) → bed
Arguments: var — Variable that controls the decision.; left — True branch (a bed).; right — False branch (a bed).

Definitions and Theorems

Function: mk-var-raw$inline

(defun mk-var-raw$inline (var left right)
  (declare (xargs :guard t))
  (let ((__function__ 'mk-var-raw))
    (declare (ignorable __function__))
    (hons var (hons left right))))

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

(defthm bed-eval-of-mk-var-raw
  (equal (bed-eval (mk-var-raw var left right)
                   env)
         (if (bed-env-lookup var env)
             (bed-eval left env)
           (bed-eval right env))))