		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-prose-val

A prose-val parse tree is abstracted to its corresponding prose value notation.

Signature
(abstract-prose-val tree) → prose-val
Arguments: tree — Guard (treep tree).
Returns: prose-val — Type (prose-val-p prose-val).

Definitions and Theorems

Function: abstract-prose-val

(defun abstract-prose-val (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) (prose-val "")))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))
                     (consp (cddr treess))))
        (fail))
       (trees (cadr treess))
       (nats (abstract-*-grouped-terminal trees))
       ((unless (unsigned-byte-listp 8 nats))
        (fail)))
    (prose-val (nats=>string nats))))

Theorem: prose-val-p-of-abstract-prose-val

(defthm prose-val-p-of-abstract-prose-val
  (b* ((prose-val (abstract-prose-val tree)))
    (prose-val-p prose-val))
  :rule-classes :rewrite)