		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Interp-st-field-p

This is an ordinary defenum.

Function: interp-st-field-p

(defun interp-st-field-p (x)
  (declare (xargs :guard t))
  (or (eq x ':stack)
      (eq x ':logicman)
      (eq x ':bvar-db)
      (eq x ':pathcond)
      (eq x ':constraint)
      (eq x ':constraint-db)
      (eq x ':prof)
      (eq x ':backchain-limit)
      (eq x ':equiv-contexts)
      (eq x ':reclimit)
      (eq x ':config)
      (eq x ':flags)
      (eq x ':fgarrays)
      (eq x ':next-fgarray)
      (eq x ':cgraph)
      (eq x ':cgraph-memo)
      (eq x ':cgraph-index)
      (eq x ':ctrex-env)
      (eq x ':sat-ctrex)
      (eq x ':user-scratch)
      (eq x ':trace-scratch)
      (eq x ':errmsg)
      (eq x ':debug-info)
      (eq x ':debug-stack)))

Theorem: type-when-interp-st-field-p

(defthm type-when-interp-st-field-p
  (implies (interp-st-field-p x)
           (if (symbolp x)
               (if (not (equal x 't))
                   (not (equal x 'nil))
                 'nil)
             'nil))
  :rule-classes :compound-recognizer)