An irrelevant ATJ type, usable as dummy return value with hard errors.
(atj-type-irrelevant) → type
Function:
(defun atj-type-irrelevant nil (declare (xargs :guard t)) (let ((__function__ 'atj-type-irrelevant)) (declare (ignorable __function__)) (with-guard-checking :none (ec-call (atj-type-fix :irrelevant)))))
Theorem:
(defthm atj-typep-of-atj-type-irrelevant (b* ((type (atj-type-irrelevant))) (atj-typep type)) :rule-classes :rewrite)