		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-to-faig

Faig-const-fix

Identity for FAIG constants, or constant X otherwise.

Signature
(faig-const-fix x) → *

Note that an older version of this function independently coerced the car/cdr of t to a Booleans when they were conses, but it seems simpler to just say anything malformed gets fixed to X.

Definitions and Theorems

Function: faig-const-fix

(defun faig-const-fix (x)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-const-fix))
    (declare (ignorable __function__))
    (if (faig-const-p x) x (faig-x))))

Theorem: faig-const-fix-of-faig-eval

(defthm faig-const-fix-of-faig-eval
  (equal (faig-const-fix (faig-eval x env))
         (faig-eval x env)))

Theorem: faig-const-p-of-faig-const-fix

(defthm faig-const-p-of-faig-const-fix
  (faig-const-p (faig-const-fix x)))

Theorem: faig-const-fix-of-faig-const

(defthm faig-const-fix-of-faig-const
  (implies (faig-const-p x)
           (equal (faig-const-fix x) x)))