		Search-engine friendly clone of the ACL2 documentation.

Irr-plexeme

An irrelevant preprocessing lexeme.

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

Function: irr-plexeme

(defun irr-plexeme nil
  (declare (xargs :guard t))
  (plexeme-ident (ident :irrelevant)))

Theorem: plexemep-of-irr-plexeme

(defthm plexemep-of-irr-plexeme
  (b* ((acl2::irr (irr-plexeme)))
    (plexemep acl2::irr))
  :rule-classes :rewrite)