		Search-engine friendly clone of the ACL2 documentation.

Hexadecimal-digits-grammar-validation

Hex-digit-tree

Tree for a hexadecimal digit.

Signature
(hex-digit-tree digit) → tree
Arguments: digit — Guard (hex-digitp digit).
Returns: tree — Type (abnf-tree-with-root-p tree "hex-digit").

This is used in grammar-hex-digitp-when-hex-digitp.

Definitions and Theorems

Function: hex-digit-tree

(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: return-type-of-hex-digit-tree

(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: tree->string-of-hex-digit-tree

(defthm tree->string-of-hex-digit-tree
  (equal (abnf::tree->string (hex-digit-tree digit))
         (list (hex-digit-fix digit))))

Theorem: hex-digit-tree-of-hex-digit-fix-digit

(defthm hex-digit-tree-of-hex-digit-fix-digit
  (equal (hex-digit-tree (hex-digit-fix digit))
         (hex-digit-tree digit)))

Theorem: hex-digit-tree-hex-digit-equiv-congruence-on-digit

(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)