Recognizer for univ-char-name structures.
(univ-char-name-p x) → *
Function:
(defun univ-char-name-p (x) (declare (xargs :guard t)) (let ((__function__ 'univ-char-name-p)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :locase-u)) (and (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((quad (std::da-nth 0 (cdr x)))) (hex-quad-p quad)))) (t (and (eq (car x) :upcase-u) (and (true-listp (cdr x)) (eql (len (cdr x)) 2)) (b* ((quad1 (std::da-nth 0 (cdr x))) (quad2 (std::da-nth 1 (cdr x)))) (and (hex-quad-p quad1) (hex-quad-p quad2)))))))))
Theorem:
(defthm consp-when-univ-char-name-p (implies (univ-char-name-p x) (consp x)) :rule-classes :compound-recognizer)