		Search-engine friendly clone of the ACL2 documentation.

Abstraction-mapping

Abs-lowercase-letter

Abstract a lowercase-letter CST to an ACL2 lowercase letter character.

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

Definitions and Theorems

Function: abs-lowercase-letter

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

Theorem: characterp-of-abs-lowercase-letter

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

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

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

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

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