		Search-engine friendly clone of the ACL2 documentation.

Parser

Lex-group-comment/ws

Lex ( comment / ws ).

Signature
(lex-group-comment/ws input) → (mv ret-tree ret-input)
Arguments: input — Guard (nat-listp input).
Returns: ret-tree — Type (abnf::tree-resultp ret-tree).; ret-input — Type (nat-listp ret-input).

Definitions and Theorems

Function: lex-group-comment/ws

(defun lex-group-comment/ws (input)
 (declare (xargs :guard (nat-listp input)))
 (let ((__function__ 'lex-group-comment/ws))
   (declare (ignorable __function__))
   (b* (((mv tree1 input1) (lex-comment input))
        ((when (not (reserrp tree1)))
         (mv (abnf::make-tree-nonleaf :rulename? nil
                                      :branches (list (list tree1)))
             input1))
        ((mv tree2 input2) (lex-ws input))
        ((when (not (reserrp tree2)))
         (mv (abnf::make-tree-nonleaf :rulename? nil
                                      :branches (list (list tree2)))
             input2)))
     (mv (reserrf (list :found (list tree1 tree2)
                        :required "( comment / ws )"))
         (nat-list-fix input)))))

Theorem: tree-resultp-of-lex-group-comment/ws.ret-tree

(defthm tree-resultp-of-lex-group-comment/ws.ret-tree
  (b* (((mv ?ret-tree ?ret-input)
        (lex-group-comment/ws input)))
    (abnf::tree-resultp ret-tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-group-comment/ws.ret-input

(defthm nat-listp-of-lex-group-comment/ws.ret-input
  (b* (((mv ?ret-tree ?ret-input)
        (lex-group-comment/ws input)))
    (nat-listp ret-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-group-comment/ws-<=

(defthm len-of-lex-group-comment/ws-<=
  (b* (((mv ?ret-tree ?ret-input)
        (lex-group-comment/ws input)))
    (<= (len ret-input) (len input)))
  :rule-classes :linear)

Theorem: lex-group-comment/ws-of-nat-list-fix-input

(defthm lex-group-comment/ws-of-nat-list-fix-input
  (equal (lex-group-comment/ws (nat-list-fix input))
         (lex-group-comment/ws input)))

Theorem: lex-group-comment/ws-nat-list-equiv-congruence-on-input

(defthm lex-group-comment/ws-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (lex-group-comment/ws input)
                  (lex-group-comment/ws input-equiv)))
  :rule-classes :congruence)