		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-alpha

An ALPHA parse tree is abstracted to its corresponding letter.

Signature
(abstract-alpha tree) → letter
Arguments: tree — Guard (treep tree).
Returns: letter — Type (characterp letter).

Definitions and Theorems

Function: abstract-alpha

(defun abstract-alpha (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) (code-char 0)))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees))
       (nat (abstract-terminal subtree))
       ((unless (< nat 256)) (fail)))
    (code-char nat)))

Theorem: characterp-of-abstract-alpha

(defthm characterp-of-abstract-alpha
  (b* ((letter (abstract-alpha tree)))
    (characterp letter))
  :rule-classes :rewrite)