		Search-engine friendly clone of the ACL2 documentation.

Amb?-declor/absdeclor

Amb?-declor/absdeclor-p

Recognizer for amb?-declor/absdeclor structures.

Signature
(amb?-declor/absdeclor-p x) → *

Definitions and Theorems

Function: amb?-declor/absdeclor-p

(defun amb?-declor/absdeclor-p (x)
 (declare (xargs :guard t))
 (and
     (consp x)
     (cond ((or (atom x) (eq (car x) :declor))
            (and (b* ((declor (cdr x)))
                   (declorp declor))))
           ((eq (car x) :absdeclor)
            (and (b* ((absdeclor (cdr x)))
                   (absdeclorp absdeclor))))
           (t (and (eq (car x) :ambig)
                   (and)
                   (b* ((declor/absdeclor (cdr x)))
                     (amb-declor/absdeclor-p declor/absdeclor)))))))

Theorem: consp-when-amb?-declor/absdeclor-p

(defthm consp-when-amb?-declor/absdeclor-p
  (implies (amb?-declor/absdeclor-p x)
           (consp x))
  :rule-classes :compound-recognizer)