		Search-engine friendly clone of the ACL2 documentation.

Irr-asm-name-spec

An irrelevant assembler name specifier.

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

Function: irr-asm-name-spec

(defun irr-asm-name-spec nil
  (declare (xargs :guard t))
  (asm-name-spec nil (keyword-uscores-none)))

Theorem: asm-name-specp-of-irr-asm-name-spec

(defthm asm-name-specp-of-irr-asm-name-spec
  (b* ((acl2::irr (irr-asm-name-spec)))
    (asm-name-specp acl2::irr))
  :rule-classes :rewrite)