		Search-engine friendly clone of the ACL2 documentation.

Irr-bexprefix

An irrelevant binary exponent prefix.

This can be used as a dummy value of the type.

Function: irr-bexprefix

(defun irr-bexprefix nil
  (declare (xargs :guard t))
  (bexprefix-locase-p))

Theorem: bexprefixp-of-irr-bexprefix

(defthm bexprefixp-of-irr-bexprefix
  (b* ((acl2::irr (irr-bexprefix)))
    (bexprefixp acl2::irr))
  :rule-classes :rewrite)