		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-terminals

A term parse tree, where term is a terminal numeric or character value notation, is generally abstracted to its list of natural numbers.

Signature
(abstract-terminals tree) → nats
Arguments: tree — Guard (treep tree).
Returns: nats — Type (nat-listp nats).

The parse tree must be a leaf labeled by a list of natural numbers. That list of natural numbers is returned.

Definitions and Theorems

Function: abstract-terminals

(defun abstract-terminals (tree)
  (declare (xargs :guard (treep tree)))
  (if (tree-case tree :leafterm)
      (tree-leafterm->get tree)
    (abstract-fail)))

Theorem: nat-listp-of-abstract-terminals

(defthm nat-listp-of-abstract-terminals
  (b* ((nats (abstract-terminals tree)))
    (nat-listp nats))
  :rule-classes :rewrite)