		Search-engine friendly clone of the ACL2 documentation.

String-kinds

Nonempty-stringp

Recognize non-empty strings.

Signature
(nonempty-stringp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: nonempty-stringp

(defun nonempty-stringp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'nonempty-stringp))
    (declare (ignorable __function__))
    (not (equal (str-fix x) ""))))

Theorem: booleanp-of-nonempty-stringp

(defthm booleanp-of-nonempty-stringp
  (b* ((yes/no (nonempty-stringp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: stringp-when-nonempty-stringp

(defthm stringp-when-nonempty-stringp
  (implies (nonempty-stringp x)
           (stringp x)))

Subtopics

Nonempty-string-listp: Recognize true lists of nonempty strings.