Tree for a hexadecimal digit.
(hex-digit-tree digit) → tree
This is used in grammar-hex-digitp-when-hex-digitp.
Function:
(defun hex-digit-tree (digit) (declare (xargs :guard (hex-digitp digit))) (let ((__function__ 'hex-digit-tree)) (declare (ignorable __function__)) (abnf::tree-nonleaf (abnf::rulename "hex-digit") (list (list (abnf::tree-leafterm (list (hex-digit-fix digit))))))))
Theorem:
(defthm return-type-of-hex-digit-tree (b* ((tree (hex-digit-tree digit))) (abnf-tree-with-root-p tree "hex-digit")) :rule-classes :rewrite)
Theorem:
(defthm tree->string-of-hex-digit-tree (equal (abnf::tree->string (hex-digit-tree digit)) (list (hex-digit-fix digit))))
Theorem:
(defthm hex-digit-tree-of-hex-digit-fix-digit (equal (hex-digit-tree (hex-digit-fix digit)) (hex-digit-tree digit)))
Theorem:
(defthm hex-digit-tree-hex-digit-equiv-congruence-on-digit (implies (hex-digit-equiv digit digit-equiv) (equal (hex-digit-tree digit) (hex-digit-tree digit-equiv))) :rule-classes :congruence)