Recognizer for natoption/natoptionlist-result structures.
(natoption/natoptionlist-resultp x) → *
Function:
(defun natoption/natoptionlist-resultp (x) (declare (xargs :guard t)) (let ((__function__ 'natoption/natoptionlist-resultp)) (declare (ignorable __function__)) (cond ((natoption/natoptionlist-p x) (b* ((get x)) (natoption/natoptionlist-p get))) (t (b* ((get x)) (fty::reserrp get))))))
Theorem:
(defthm consp-when-natoption/natoptionlist-resultp (implies (natoption/natoptionlist-resultp x) (consp x)) :rule-classes :compound-recognizer)