		Search-engine friendly clone of the ACL2 documentation.

Fgl-env

Fgl-env-p

Recognizer for fgl-env structures.

Signature
(fgl-env-p x) → *

Definitions and Theorems

Function: fgl-env-p

(defun fgl-env-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'fgl-env-p))
    (declare (ignorable __function__))
    (and (std::prod-consp x)
         (b* ((obj-alist (std::prod-car x))
              (?bfr-vals (std::prod-cdr x)))
           (obj-alist-p obj-alist)))))