		Search-engine friendly clone of the ACL2 documentation.

Maybe-stringp

Recognizer for strings and nil.

This is like an option type; when x satisfies maybe-stringp, then either it is a string or nothing.

Function: maybe-stringp$inline

(defun maybe-stringp$inline (x)
  (declare (xargs :guard t))
  (or (not x) (stringp x)))

Theorem: maybe-stringp-compound-recognizer

(defthm maybe-stringp-compound-recognizer
  (equal (maybe-stringp x)
         (or (not x) (stringp x)))
  :rule-classes :compound-recognizer)