An irrelevant quadruple of hexadecimal digits.
(irr-hex-quad) → acl2::irr
This can be used as a dummy value of the type.
Function:
(defun irr-hex-quad nil (declare (xargs :guard t)) (let ((__function__ 'irr-hex-quad)) (declare (ignorable __function__)) (make-hex-quad :1st #\0 :2nd #\0 :3rd #\0 :4th #\0)))
Theorem:
(defthm hex-quad-p-of-irr-hex-quad (b* ((acl2::irr (irr-hex-quad))) (hex-quad-p acl2::irr)) :rule-classes :rewrite)