Value-resultp
Recognizer for value-result structures.
- Signature
(value-resultp acl2::x) → *
Definitions and Theorems
Function: value-resultp
(defun value-resultp (acl2::x)
(declare (xargs :guard t))
(cond ((valuep acl2::x)
(b* ((get acl2::x)) (valuep get)))
(t (b* ((get acl2::x)) (errorp get)))))
