Check if the features indicate little endian.
Function:
(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:
(defthm booleanp-of-feat-little-endianp (b* ((yes/no (feat-little-endianp feat))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm feat-little-endianp-of-feat-fix-feat (equal (feat-little-endianp (feat-fix feat)) (feat-little-endianp feat)))
Theorem:
(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)