		Search-engine friendly clone of the ACL2 documentation.

Specialized-features

Feat-rv32e-le

Features for RV32E, with little endian memory.

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

Definitions and Theorems

Function: feat-rv32e-le

(defun feat-rv32e-le nil
  (declare (xargs :guard t))
  (make-feat :base (feat-base-rv32e)
             :endian (feat-endian-little)
             :m nil))

Theorem: featp-of-feat-rv32e-le

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