		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-*digit

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

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

Definitions and Theorems

Function: abstract-*digit-aux

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

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

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

Function: abstract-*digit

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

Theorem: natp-of-abstract-*digit

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