		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-grouped-terminal

A ( term1 / ... / termN ) parse tree, where term1, ..., termN are terminal numeric and character notations that all denote single natural numbers, is sometimes abstracted to its only natural number.

Signature
(abstract-grouped-terminal tree) → nat
Arguments: tree — Guard (treep tree).
Returns: nat — Type (natp nat).

The 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.

Definitions and Theorems

Function: abstract-grouped-terminal

(defun abstract-grouped-terminal (tree)
  (declare (xargs :guard (treep tree)))
  (b* ((nats (abstract-grouped-terminals tree)))
    (if (consp nats)
        (car nats)
      (prog2$ (abstract-fail) 0))))

Theorem: natp-of-abstract-grouped-terminal

(defthm natp-of-abstract-grouped-terminal
  (b* ((nat (abstract-grouped-terminal tree)))
    (natp nat))
  :rule-classes :rewrite)