		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-lowercaseletter/decimaldigit

Abstract a *( lowercase-letter / decimal-digit ) to a list of ACL2 characters.

Signature
(abs-*-lowercaseletter/decimaldigit trees) → chars
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: chars — Type (character-list-resultp chars).

Definitions and Theorems

Function: abs-*-lowercaseletter/decimaldigit

(defun abs-*-lowercaseletter/decimaldigit (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-lowercaseletter/decimaldigit))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf char)
          (abs-lowercaseletter/decimaldigit (car trees)))
         ((okf chars)
          (abs-*-lowercaseletter/decimaldigit (cdr trees))))
      (cons char chars))))

Theorem: character-list-resultp-of-abs-*-lowercaseletter/decimaldigit

(defthm character-list-resultp-of-abs-*-lowercaseletter/decimaldigit
  (b* ((chars (abs-*-lowercaseletter/decimaldigit trees)))
    (character-list-resultp chars))
  :rule-classes :rewrite)

Theorem: loletter/digit-char-listp-of-abs-*-lowercaseletter/decimaldigit

(defthm
    loletter/digit-char-listp-of-abs-*-lowercaseletter/decimaldigit
  (b* ((?chars (abs-*-lowercaseletter/decimaldigit trees)))
    (implies (not (reserrp chars))
             (str::lcletter/digit-charlist-p chars))))

Theorem: abs-*-lowercaseletter/decimaldigit-of-tree-list-fix-trees

(defthm abs-*-lowercaseletter/decimaldigit-of-tree-list-fix-trees
 (equal
    (abs-*-lowercaseletter/decimaldigit (abnf::tree-list-fix trees))
    (abs-*-lowercaseletter/decimaldigit trees)))

Theorem: abs-*-lowercaseletter/decimaldigit-tree-list-equiv-congruence-on-trees

(defthm
 abs-*-lowercaseletter/decimaldigit-tree-list-equiv-congruence-on-trees
 (implies (abnf::tree-list-equiv trees trees-equiv)
          (equal (abs-*-lowercaseletter/decimaldigit trees)
                 (abs-*-lowercaseletter/decimaldigit trees-equiv)))
 :rule-classes :congruence)