		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-bin-val-rest

A [ 1*("." 1*BIT) / ("-" 1*BIT) ] parse tree is abstracted to either the list of its big-endian values (for the first alternative) or its single big-endian value (for the second alternative).

Signature
(abstract-bin-val-rest tree) → result
Arguments: tree — Guard (treep tree).
Returns: result — Type (or (nat-listp result) (natp result)).

Definitions and Theorems

Function: abstract-bin-val-rest

(defun abstract-bin-val-rest (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail)) (abstract-fail))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((when (endp treess)) nil)
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (1st-subtree (car trees)))
    (if (abstract-bin/dec/hex-val-rest-dot-p 1st-subtree)
        (abstract-*-dot-1*bit trees)
      (abstract-dot/dash-1*bit 1st-subtree))))

Theorem: return-type-of-abstract-bin-val-rest

(defthm return-type-of-abstract-bin-val-rest
  (b* ((result (abstract-bin-val-rest tree)))
    (or (nat-listp result) (natp result)))
  :rule-classes :rewrite)