		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Bed-match-var

Pattern match a variable ITE node.

Signature
(bed-match-var x) → (mv okp var left right)
Arguments: x — The BED to pattern match against.
Returns: okp — Whether or not we matched a variable.; var — On success, the variable we matched.; left — On success, the true branch for this variable.; right — On success, the false branch for this variable.

Definitions and Theorems

Function: bed-match-var

(defun bed-match-var (x)
  (declare (xargs :guard t))
  (let ((__function__ 'bed-match-var))
    (declare (ignorable __function__))
    (if (and (consp x) (not (integerp (cdr x))))
        (mv t (car x)
            (car$ (cdr x))
            (cdr$ (cdr x)))
      (mv nil nil nil nil))))

Theorem: bed-match-var-correct

(defthm bed-match-var-correct
  (b* (((mv okp var left right)
        (bed-match-var x)))
    (implies okp
             (equal (bed-eval x env)
                    (if (bed-env-lookup var env)
                        (bed-eval left env)
                      (bed-eval right env))))))