		Search-engine friendly clone of the ACL2 documentation.

Hex-core-fconst

Hex-core-fconstp

Recognizer for hex-core-fconst structures.

Signature
(hex-core-fconstp x) → *

Definitions and Theorems

Function: hex-core-fconstp

(defun hex-core-fconstp (x)
  (declare (xargs :guard t))
  (and (consp x)
       (cond ((or (atom x) (eq (car x) :frac))
              (and (consp (cdr x))
                   (b* ((significand (car (cdr x)))
                        (expo (cdr (cdr x))))
                     (and (hex-frac-constp significand)
                          (bin-expop expo)))))
             (t (and (eq (car x) :int)
                     (and (consp (cdr x)))
                     (b* ((significand (car (cdr x)))
                          (expo (cdr (cdr x))))
                       (and (hex-digit-char-listp significand)
                            (bin-expop expo))))))))

Theorem: consp-when-hex-core-fconstp

(defthm consp-when-hex-core-fconstp
  (implies (hex-core-fconstp x) (consp x))
  :rule-classes :compound-recognizer)