		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-58-lcletter/decdigit

Lex a 58( lowercase-letter / decimal-digit ).

Signature
(lex-58-lcletter/decdigit input) → (mv trees rest-input)
Arguments: input — Guard (nat-listp input).
Returns: trees — Type (abnf::tree-list-resultp trees).; rest-input — Type (nat-listp rest-input).

Definitions and Theorems

Function: lex-58-lcletter/decdigit

(defun lex-58-lcletter/decdigit (input)
  (declare (xargs :guard (nat-listp input)))
  (let ((__function__ 'lex-58-lcletter/decdigit))
    (declare (ignorable __function__))
    (b* (((mv trees input1)
          (lex-*-lcletter/decdigit input))
         ((unless (= (len trees) 58))
          (mv (reserrf (list :found trees :required 58))
              (nat-list-fix input))))
      (mv trees input1))))

Theorem: tree-list-resultp-of-lex-58-lcletter/decdigit.trees

(defthm tree-list-resultp-of-lex-58-lcletter/decdigit.trees
  (b* (((mv ?trees ?rest-input)
        (lex-58-lcletter/decdigit input)))
    (abnf::tree-list-resultp trees))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-58-lcletter/decdigit.rest-input

(defthm nat-listp-of-lex-58-lcletter/decdigit.rest-input
  (b* (((mv ?trees ?rest-input)
        (lex-58-lcletter/decdigit input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-58-lcletter/decdigit-<=

(defthm len-of-lex-58-lcletter/decdigit-<=
  (b* (((mv ?trees ?rest-input)
        (lex-58-lcletter/decdigit input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-lex-58-lcletter/decdigit-<

(defthm len-of-lex-58-lcletter/decdigit-<
  (b* (((mv ?trees ?rest-input)
        (lex-58-lcletter/decdigit input)))
    (implies (not (reserrp trees))
             (<= (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: lex-58-lcletter/decdigit-of-nat-list-fix-input

(defthm lex-58-lcletter/decdigit-of-nat-list-fix-input
  (equal (lex-58-lcletter/decdigit (nat-list-fix input))
         (lex-58-lcletter/decdigit input)))

Theorem: lex-58-lcletter/decdigit-nat-list-equiv-congruence-on-input

(defthm lex-58-lcletter/decdigit-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (lex-58-lcletter/decdigit input)
                  (lex-58-lcletter/decdigit input-equiv)))
  :rule-classes :congruence)