		Search-engine friendly clone of the ACL2 documentation.

Execution32

Feat-rv32im

Features for RV32IM.

Signature
(feat-rv32im) → feat
Returns: feat — Type (featp feat).

Definitions and Theorems

Function: feat-rv32im

(defun feat-rv32im nil
  (declare (xargs :guard t))
  (let ((__function__ 'feat-rv32im))
    (declare (ignorable __function__))
    (make-feat :bits (feat-bits-32))))

Theorem: featp-of-feat-rv32im

(defthm featp-of-feat-rv32im
  (b* ((feat (feat-rv32im))) (featp feat))
  :rule-classes :rewrite)