|
|
|---|
|
|
|
|---|
Recognizer for nat-result structures.
(nat-resultp x) → *
Function:
(defun nat-resultp (x) (declare (xargs :guard t)) (let ((__function__ 'nat-resultp)) (declare (ignorable __function__)) (cond ((natp x) (b* ((get x)) (natp get))) (t (b* ((get x)) (fty::reserrp get))))))