		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Svar-overridetype-p

This is an ordinary defenum.

Function: svar-overridetype-p

(defun svar-overridetype-p (x)
  (declare (xargs :guard t))
  (or (eq x 'nil)
      (eq x ':val)
      (eq x ':test)
      (eql x '3)
      (eql x '4)
      (eql x '5)
      (eql x '6)
      (eql x '7)))

Theorem: type-when-svar-overridetype-p

(defthm type-when-svar-overridetype-p
  (implies (svar-overridetype-p x)
           (if (if (integerp x) (< '1 x) 'nil)
               't
             (if (if (symbolp x)
                     (if (not (equal x 't))
                         (not (equal x 'nil))
                       'nil)
                   'nil)
                 't
               (equal x 'nil))))
  :rule-classes :compound-recognizer)