		Search-engine friendly clone of the ACL2 documentation.

Features

Feat-mp

Check if the features indicate the M extension.

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

Definitions and Theorems

Function: feat-mp

(defun feat-mp (feat)
  (declare (xargs :guard (featp feat)))
  (let ((__function__ 'feat-mp))
    (declare (ignorable __function__))
    (feat->m feat)))

Theorem: booleanp-of-feat-mp

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

Theorem: feat-mp-of-feat-fix-feat

(defthm feat-mp-of-feat-fix-feat
  (equal (feat-mp (feat-fix feat))
         (feat-mp feat)))

Theorem: feat-mp-feat-equiv-congruence-on-feat

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