		Search-engine friendly clone of the ACL2 documentation.

Rv64im-le-features

Feat-rv64im-le

Features for RV64IM little endian.

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

Definitions and Theorems

Function: feat-rv64im-le

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

Theorem: featp-of-feat-rv64im-le

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