		Search-engine friendly clone of the ACL2 documentation.

Features

Feat-little-endianp

Check if the features indicate little endian.

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

Definitions and Theorems

Function: feat-little-endianp

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

Theorem: booleanp-of-feat-little-endianp

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

Theorem: feat-little-endianp-of-feat-fix-feat

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

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

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

Subtopics

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