		Search-engine friendly clone of the ACL2 documentation.

Features

Feat-big-endianp

Check if the features indicate bit endian.

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

Definitions and Theorems

Function: feat-big-endianp

(defun feat-big-endianp (feat)
  (declare (xargs :guard (featp feat)))
  (let ((__function__ 'feat-big-endianp))
    (declare (ignorable __function__))
    (feat-endian-case (feat->endian feat)
                      :big)))

Theorem: booleanp-of-feat-big-endianp

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

Theorem: feat-big-endianp-of-feat-fix-feat

(defthm feat-big-endianp-of-feat-fix-feat
  (equal (feat-big-endianp (feat-fix feat))
         (feat-big-endianp feat)))

Theorem: feat-big-endianp-feat-equiv-congruence-on-feat

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

Subtopics

Feat-little-or-big-endianp: One of feat-little-endianp and feat-big-endianp always holds.