		Search-engine friendly clone of the ACL2 documentation.

Abstraction-mapping

Abs-uppercase-letter

Abstract an uppercase-letter CST to an ACL2 uppercase letter character.

Signature
(abs-uppercase-letter cst) → achar
Arguments: cst — Guard (abnf::treep cst).
Returns: achar — Type (characterp achar).

Definitions and Theorems

Function: abs-uppercase-letter

(defun abs-uppercase-letter (cst)
  (declare (xargs :guard (abnf::treep cst)))
  (declare (xargs :guard (cst-matchp cst "uppercase-letter")))
  (let ((__function__ 'abs-uppercase-letter))
    (declare (ignorable __function__))
    (b* ((cst (cst-uppercase-letter-conc-rep-elem cst))
         (nat (cst-%x41-5a-nat cst)))
      (code-char nat))))

Theorem: characterp-of-abs-uppercase-letter

(defthm characterp-of-abs-uppercase-letter
  (b* ((achar (abs-uppercase-letter cst)))
    (characterp achar))
  :rule-classes :rewrite)

Theorem: abs-uppercase-letter-of-tree-fix-cst

(defthm abs-uppercase-letter-of-tree-fix-cst
  (equal (abs-uppercase-letter (abnf::tree-fix cst))
         (abs-uppercase-letter cst)))

Theorem: abs-uppercase-letter-tree-equiv-congruence-on-cst

(defthm abs-uppercase-letter-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv cst cst-equiv)
           (equal (abs-uppercase-letter cst)
                  (abs-uppercase-letter cst-equiv)))
  :rule-classes :congruence)