		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-bin/dec/hex-val

A (bin-val / dec-val / hex-val ) parse tree is abstracted to its corresponding numeric value notation.

Signature
(abstract-bin/dec/hex-val tree) → num-val
Arguments: tree — Guard (treep tree).
Returns: num-val — Type (num-val-p num-val).

Definitions and Theorems

Function: abstract-bin/dec/hex-val

(defun abstract-bin/dec/hex-val (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail)
                (num-val-direct (num-base-bin) nil)))
       ((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))
       ((unless (tree-case subtree :nonleaf))
        (fail))
       (rulename (tree-nonleaf->rulename? subtree)))
    (cond ((equal rulename (rulename "bin-val"))
           (abstract-bin-val subtree))
          ((equal rulename (rulename "dec-val"))
           (abstract-dec-val subtree))
          (t (abstract-hex-val subtree)))))

Theorem: num-val-p-of-abstract-bin/dec/hex-val

(defthm num-val-p-of-abstract-bin/dec/hex-val
  (b* ((num-val (abstract-bin/dec/hex-val tree)))
    (num-val-p num-val))
  :rule-classes :rewrite)