		Search-engine friendly clone of the ACL2 documentation.

Abstraction-mapping

Abs-digit

Abstract a digit CST to an ACL2 digit character.

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

Definitions and Theorems

Function: abs-digit

(defun abs-digit (cst)
  (declare (xargs :guard (abnf::treep cst)))
  (declare (xargs :guard (cst-matchp cst "digit")))
  (let ((__function__ 'abs-digit))
    (declare (ignorable __function__))
    (b* ((cst (cst-digit-conc-rep-elem cst))
         (nat (cst-%x30-39-nat cst)))
      (code-char nat))))

Theorem: characterp-of-abs-digit

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

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

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

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

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