		Search-engine friendly clone of the ACL2 documentation.

Numbered-name-index-start

Numbered-name-index-start-p

Recognize admissible starting markers of the numeric index of numbered names.

Signature
(numbered-name-index-start-p x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Check whether x consists of one or more non-numeric characters.

Definitions and Theorems

Function: numbered-name-index-start-p

(defun numbered-name-index-start-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'numbered-name-index-start-p))
    (declare (ignorable __function__))
    (and (stringp x)
         (str::nondigit-charlist-p (explode x))
         (not (equal x "")))))

Theorem: booleanp-of-numbered-name-index-start-p

(defthm booleanp-of-numbered-name-index-start-p
  (b* ((yes/no (numbered-name-index-start-p x)))
    (booleanp yes/no))
  :rule-classes :rewrite)