		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-*hexdig

A list of zero or more HEXDIG parse trees is abstracted to the big-endian value of its hexadecimal digits.

Signature
(abstract-*hexdig trees) → nat
Arguments: trees — Guard (tree-listp trees).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: abstract-*hexdig-aux

(defun abstract-*hexdig-aux (trees accumulator)
  (declare (xargs :guard (and (tree-listp trees)
                              (natp accumulator))))
  (b* (((when (endp trees)) (nfix accumulator))
       (hexdig (abstract-hexdig (car trees))))
    (abstract-*hexdig-aux (cdr trees)
                          (+ (* 16 accumulator) hexdig))))

Theorem: natp-of-abstract-*hexdig-aux

(defthm natp-of-abstract-*hexdig-aux
  (b* ((nat (abstract-*hexdig-aux trees accumulator)))
    (natp nat))
  :rule-classes :rewrite)

Function: abstract-*hexdig

(defun abstract-*hexdig (trees)
  (declare (xargs :guard (tree-listp trees)))
  (abstract-*hexdig-aux trees 0))

Theorem: natp-of-abstract-*hexdig

(defthm natp-of-abstract-*hexdig
  (b* ((nat (abstract-*hexdig trees)))
    (natp nat))
  :rule-classes :rewrite)