Abstract a
(abs-letter/decimaldigit/underscore tree) → char
Function:
(defun abs-letter/decimaldigit/underscore (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-letter/decimaldigit/underscore)) (declare (ignorable __function__)) (b* (((okf tree) (check-tree-nonleaf-1-1 tree nil)) (char (abs-letter tree)) ((when (not (reserrp char))) char) (char (abs-decimal-digit-to-char tree)) ((when (not (reserrp char))) char) (pass (check-tree-ichars tree "_")) ((when (not (reserrp pass))) #\_)) (reserrf (list :found-subtree (tree-info-for-error tree))))))
Theorem:
(defthm character-resultp-of-abs-letter/decimaldigit/underscore (b* ((char (abs-letter/decimaldigit/underscore tree))) (character-resultp char)) :rule-classes :rewrite)
Theorem:
(defthm letter/digit/uscore-char-p-of-abs-letter/decimaldigit/underscore (b* ((common-lisp::?char (abs-letter/decimaldigit/underscore tree))) (implies (not (reserrp char)) (str::letter/digit/uscore-char-p char))))
Theorem:
(defthm abs-letter/decimaldigit/underscore-of-tree-fix-tree (equal (abs-letter/decimaldigit/underscore (abnf::tree-fix tree)) (abs-letter/decimaldigit/underscore tree)))
Theorem:
(defthm abs-letter/decimaldigit/underscore-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-letter/decimaldigit/underscore tree) (abs-letter/decimaldigit/underscore tree-equiv))) :rule-classes :congruence)