		Search-engine friendly clone of the ACL2 documentation.

Irr-dexpo

An irrelevant decimal exponent.

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

Function: irr-dexpo

(defun irr-dexpo nil
  (declare (xargs :guard t))
  (make-dexpo :prefix (irr-dexprefix)
              :sign? nil
              :digits nil))

Theorem: dexpop-of-irr-dexpo

(defthm dexpop-of-irr-dexpo
  (b* ((acl2::irr (irr-dexpo)))
    (dexpop acl2::irr))
  :rule-classes :rewrite)