Recognizer for dec/oct/hex-const structures.
(dec/oct/hex-constp x) → *
Function:
(defun dec/oct/hex-constp (x) (declare (xargs :guard t)) (let ((__function__ 'dec/oct/hex-constp)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :dec)) (and (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((value (std::da-nth 0 (cdr x)))) (posp value)))) ((eq (car x) :oct) (and (true-listp (cdr x)) (eql (len (cdr x)) 2) (b* ((leading-zeros (std::da-nth 0 (cdr x))) (value (std::da-nth 1 (cdr x)))) (and (posp leading-zeros) (natp value))))) (t (and (eq (car x) :hex) (and (true-listp (cdr x)) (eql (len (cdr x)) 2)) (b* ((prefix (std::da-nth 0 (cdr x))) (digits (std::da-nth 1 (cdr x)))) (and (hprefixp prefix) (hex-digit-char-listp digits)))))))))
Theorem:
(defthm consp-when-dec/oct/hex-constp (implies (dec/oct/hex-constp x) (consp x)) :rule-classes :compound-recognizer)