		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Fgl-prog2

In the FGL interpreter, run the first form for side effects and return the result from the second form.

Signature
(fgl-prog2 x y) → *

Logically, returns the second argument. In FGL, the first argument is interpreted under the unequiv equivalence context, then the second is interpreted normally and returned.

Definitions and Theorems

Function: fgl-prog2

(defun fgl-prog2 (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'fgl-prog2))
    (declare (ignorable __function__))
    y))

Theorem: unequiv-implies-equal-fgl-prog2-1

(defthm unequiv-implies-equal-fgl-prog2-1
  (implies (unequiv x x-equiv)
           (equal (fgl-prog2 x y)
                  (fgl-prog2 x-equiv y)))
  :rule-classes (:congruence))