Included Books
other
(in-package "ACL2")
include-book
(include-book "defirrelevant")
other
(defirrelevant irr-integer :short "An irrelevant integer." :type integerp :body 0)
other
(defirrelevant irr-symbol :short "An irrelevant symbol." :type symbolp :body nil)