		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Special-term-num

Signature
(special-term-num sym) → i
Arguments: sym — Guard (symbolp sym).
Returns: i — Type (or (null i) (natp i)).

Definitions and Theorems

Function: special-term-num

(defun special-term-num (sym)
  (declare (xargs :guard (symbolp sym)))
  (let ((acl2::__function__ 'special-term-num))
    (declare (ignorable acl2::__function__))
    (let ((special-term-num (cdr (assoc sym *ppr-special-syms*))))
      (if (null special-term-num)
          nil
        (if (natp special-term-num)
            special-term-num
          (illegal 'special-term-num
                   "Value for ~x0 is ~x1. Should be NIL or natp"
                   (list (cons #\0 sym)
                         (cons #\1 special-term-num))))))))

Theorem: return-type-of-special-term-num

(defthm return-type-of-special-term-num
  (b* ((i (special-term-num sym)))
    (or (null i) (natp i)))
  :rule-classes :rewrite)