		Search-engine friendly clone of the ACL2 documentation.

Features

Feat-rv64em-be

Features for RV64EM, with big endian memory.

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

Definitions and Theorems

Function: feat-rv64em-be

(defun feat-rv64em-be nil
  (declare (xargs :guard t))
  (let ((__function__ 'feat-rv64em-be))
    (declare (ignorable __function__))
    (make-feat :base (feat-base-rv64e)
               :endian (feat-endian-big)
               :m t)))

Theorem: featp-of-feat-rv64em-be

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