Abstract a
(abs-decimal-digit-to-char tree) → char
Function:
(defun abs-decimal-digit-to-char (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-decimal-digit-to-char)) (declare (ignorable __function__)) (b* (((okf nat) (check-tree-nonleaf-num-range tree "digit" 48 57))) (code-char nat))))
Theorem:
(defthm character-resultp-of-abs-decimal-digit-to-char (b* ((char (abs-decimal-digit-to-char tree))) (character-resultp char)) :rule-classes :rewrite)
Theorem:
(defthm dec-digit-char-p-of-abs-decimal-digit-to-char (b* ((common-lisp::?char (abs-decimal-digit-to-char tree))) (implies (not (reserrp char)) (str::dec-digit-char-p char))))
Theorem:
(defthm abs-decimal-digit-to-char-of-tree-fix-tree (equal (abs-decimal-digit-to-char (abnf::tree-fix tree)) (abs-decimal-digit-to-char tree)))
Theorem:
(defthm abs-decimal-digit-to-char-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-decimal-digit-to-char tree) (abs-decimal-digit-to-char tree-equiv))) :rule-classes :congruence)