		Search-engine friendly clone of the ACL2 documentation.

Features

Feat->xlen

The XLEN parameter [ISA:1.3].

Signature
(feat->xlen feat) → xlen
Arguments: feat — Guard (featp feat).
Returns: xlen — Type (posp xlen).

This is the register width, depending on the choice of base.

Definitions and Theorems

Function: feat->xlen

(defun feat->xlen (feat)
  (declare (xargs :guard (featp feat)))
  (let ((__function__ 'feat->xlen))
    (declare (ignorable __function__))
    (b* (((feat feat) feat))
      (feat-bits-case feat.bits
                      :|32| 32
                      :|64| 64))))

Theorem: posp-of-feat->xlen

(defthm posp-of-feat->xlen
  (b* ((xlen (feat->xlen feat)))
    (posp xlen))
  :rule-classes (:rewrite :type-prescription))

Theorem: feat->xlen-when-32-bits

(defthm feat->xlen-when-32-bits
  (implies (feat-bits-case (feat->bits feat) :|32|)
           (b* ((?xlen (feat->xlen feat)))
             (equal xlen 32))))

Theorem: feat->xlen-when-64-bits

(defthm feat->xlen-when-64-bits
  (implies (feat-bits-case (feat->bits feat) :|64|)
           (b* ((?xlen (feat->xlen feat)))
             (equal xlen 64))))

Theorem: feat->xlen-of-feat-fix-feat

(defthm feat->xlen-of-feat-fix-feat
  (equal (feat->xlen (feat-fix feat))
         (feat->xlen feat)))

Theorem: feat->xlen-feat-equiv-congruence-on-feat

(defthm feat->xlen-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (feat->xlen feat)
                  (feat->xlen feat-equiv)))
  :rule-classes :congruence)