		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))