		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Check-optional-minus-sign-p

Check if a tree is [ "-" ].

Signature
(check-optional-minus-sign-p tree) → ret
Arguments: tree — Guard (abnf::treep tree).
Returns: ret — Type (boolean-resultp ret).

Definitions and Theorems

Function: check-optional-minus-sign-p

(defun check-optional-minus-sign-p (tree)
  (declare (xargs :guard (abnf::treep tree)))
  (let ((__function__ 'check-optional-minus-sign-p))
    (declare (ignorable __function__))
    (b* (((okf treess)
          (abnf::check-tree-nonleaf tree nil))
         ((when (endp treess)) nil)
         ((okf trees)
          (abnf::check-tree-list-list-1 treess))
         ((okf tree)
          (abnf::check-tree-list-1 trees))
         (pass (abnf::check-tree-ichars tree "-"))
         ((when (reserrp pass)) pass))
      t)))

Theorem: boolean-resultp-of-check-optional-minus-sign-p

(defthm boolean-resultp-of-check-optional-minus-sign-p
  (b* ((ret (check-optional-minus-sign-p tree)))
    (boolean-resultp ret))
  :rule-classes :rewrite)

Theorem: check-optional-minus-sign-p-of-tree-fix-tree

(defthm check-optional-minus-sign-p-of-tree-fix-tree
  (equal (check-optional-minus-sign-p (abnf::tree-fix tree))
         (check-optional-minus-sign-p tree)))

Theorem: check-optional-minus-sign-p-tree-equiv-congruence-on-tree

(defthm check-optional-minus-sign-p-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (check-optional-minus-sign-p tree)
                  (check-optional-minus-sign-p tree-equiv)))
  :rule-classes :congruence)