		Search-engine friendly clone of the ACL2 documentation.

Abstraction-mapping

Abs-letter

Abstract a letter CST to an ACL2 letter character.

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

Definitions and Theorems

Function: abs-letter

(defun abs-letter (cst)
  (declare (xargs :guard (abnf::treep cst)))
  (declare (xargs :guard (cst-matchp cst "letter")))
  (let ((__function__ 'abs-letter))
    (declare (ignorable __function__))
    (case (cst-letter-conc? cst)
      (1 (abs-uppercase-letter (cst-letter-conc1-rep-elem cst)))
      (2 (abs-lowercase-letter (cst-letter-conc2-rep-elem cst))))))

Theorem: characterp-of-abs-letter

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

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

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

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

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