		Search-engine friendly clone of the ACL2 documentation.

Features

Feat-64p

Check if the features indicate 64 bits.

Signature
(feat-64p feat) → yes/no
Arguments: feat — Guard (featp feat).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: feat-64p

(defun feat-64p (feat)
  (declare (xargs :guard (featp feat)))
  (let ((__function__ 'feat-64p))
    (declare (ignorable __function__))
    (or (feat-base-case (feat->base feat)
                        :rv64i)
        (feat-base-case (feat->base feat)
                        :rv64e))))

Theorem: booleanp-of-feat-64p

(defthm booleanp-of-feat-64p
  (b* ((yes/no (feat-64p feat)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: feat-64p-of-feat-fix-feat

(defthm feat-64p-of-feat-fix-feat
  (equal (feat-64p (feat-fix feat))
         (feat-64p feat)))

Theorem: feat-64p-feat-equiv-congruence-on-feat

(defthm feat-64p-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (feat-64p feat)
                  (feat-64p feat-equiv)))
  :rule-classes :congruence)

Subtopics

Feat-32p-or-64p: One of feat-32p and feat-64p always holds.