		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-terminal

A term parse tree, where term is a terminal numeric or character value notation that denotes a single natural number, is sometimes abstracted to its only natural number.

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

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

Definitions and Theorems

Function: abstract-terminal

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

Theorem: natp-of-abstract-terminal

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