		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Fgl-toplevel-sat-check-mode-p

This is an ordinary defenum.

Function: fgl-toplevel-sat-check-mode-p

(defun fgl-toplevel-sat-check-mode-p (x)
  (declare (xargs :guard t))
  (or (eq x 't)
      (eq x 'nil)
      (eq x ':insert)))

Theorem: type-when-fgl-toplevel-sat-check-mode-p

(defthm type-when-fgl-toplevel-sat-check-mode-p
  (implies (fgl-toplevel-sat-check-mode-p x)
           (symbolp x))
  :rule-classes :compound-recognizer)