		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-*-grouped-terminal

A list of zero or more ( term1 / ... / termN ) parse trees, where term1, ..., termN are terminal numeric or character value notations that all denote single natural numbers, are abstracted to the list of its natural numbers.

Signature
(abstract-*-grouped-terminal trees) → nats
Arguments: trees — Guard (tree-listp trees).
Returns: nats — Type (nat-listp nats).

Each parse tree must have a root labeled by no rule name, with a single leaf subtree labeled by a list of one natural number. That natural number is returned in correspondence to the parse tree.

Definitions and Theorems

Function: abstract-*-grouped-terminal

(defun abstract-*-grouped-terminal (trees)
  (declare (xargs :guard (tree-listp trees)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) nil))
       ((when (endp trees)) nil)
       ((cons tree trees) trees)
       (nat (abstract-grouped-terminal tree))
       (nats (abstract-*-grouped-terminal trees)))
    (cons nat nats)))

Theorem: nat-listp-of-abstract-*-grouped-terminal

(defthm nat-listp-of-abstract-*-grouped-terminal
  (b* ((nats (abstract-*-grouped-terminal trees)))
    (nat-listp nats))
  :rule-classes :rewrite)