		Search-engine friendly clone of the ACL2 documentation.

Features

Feat->ilen

The ILEN parameter [ISA:1.5].

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

This is currently always 32, but it could be larger if we add support for more features.

Definitions and Theorems

Function: feat->ilen

(defun feat->ilen (feat)
  (declare (xargs :guard (featp feat)))
  (declare (ignore feat))
  (declare (xargs :type-prescription (and (posp (feat->ilen feat))
                                          (> (feat->ilen feat) 1))))
  (let ((__function__ 'feat->ilen))
    (declare (ignorable __function__))
    32))

Theorem: posp-of-feat->ilen

(defthm posp-of-feat->ilen
  (b* ((ilen (feat->ilen feat)))
    (posp ilen))
  :rule-classes :rewrite)

Theorem: feat->ilen-of-feat-fix-feat

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

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

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