		Search-engine friendly clone of the ACL2 documentation.

Irr-ident

An irrelevant identifier.

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

Function: irr-ident

(defun irr-ident nil
  (declare (xargs :guard t))
  (let ((__function__ 'irr-ident))
    (declare (ignorable __function__))
    (ident "_")))

Theorem: identp-of-irr-ident

(defthm identp-of-irr-ident
  (b* ((acl2::irr (irr-ident)))
    (identp acl2::irr))
  :rule-classes :rewrite)