		Search-engine friendly clone of the ACL2 documentation.

Irr-filedata

An irrelevant file data value.

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

Function: irr-filedata

(defun irr-filedata nil
  (declare (xargs :guard t))
  (filedata nil))

Theorem: filedatap-of-irr-filedata

(defthm filedatap-of-irr-filedata
  (b* ((acl2::irr (irr-filedata)))
    (filedatap acl2::irr))
  :rule-classes :rewrite)