		Search-engine friendly clone of the ACL2 documentation.

Bech32

Mixed-case-stringp

Signature
(mixed-case-stringp s) → y/n
Arguments: s — Guard (stringp s).
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: mixed-case-stringp

(defun mixed-case-stringp (s)
  (declare (xargs :guard (stringp s)))
  (let ((__function__ 'mixed-case-stringp))
    (declare (ignorable __function__))
    (and (not (equal (str::upcase-string s) s))
         (not (equal (str::downcase-string s) s)))))

Theorem: booleanp-of-mixed-case-stringp

(defthm booleanp-of-mixed-case-stringp
  (b* ((y/n (mixed-case-stringp s)))
    (booleanp y/n))
  :rule-classes :rewrite)