		Search-engine friendly clone of the ACL2 documentation.

Features

Feat-32p

Check if the features indicate 32 bits.

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

Definitions and Theorems

Function: feat-32p

(defun feat-32p (feat)
  (declare (xargs :guard (featp feat)))
  (let ((__function__ 'feat-32p))
    (declare (ignorable __function__))
    (feat-base-case (feat->base feat)
                    :rv32i)))

Theorem: booleanp-of-feat-32p

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

Theorem: feat-32p-of-feat-fix-feat

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

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

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

Subtopics

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