Recognizer for unicode-input-char structures.
(unicode-input-char-p x) → *
Function:
(defun unicode-input-char-p (x) (declare (xargs :guard t)) (let ((__function__ 'unicode-input-char-p)) (declare (ignorable __function__)) (and (consp x) (eq (car x) :unicode-input-char) (true-listp (cdr x)) (eql (len (cdr x)) 2) (b* ((unicode (std::da-nth 0 (cdr x))) (umarker (std::da-nth 1 (cdr x)))) (and (unicodep unicode) (natp umarker))))))
Theorem:
(defthm consp-when-unicode-input-char-p (implies (unicode-input-char-p x) (consp x)) :rule-classes :compound-recognizer)