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