		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-rulelist

A rulelist parse tree is abstracted to its corresponding list of rules.

Signature
(abstract-rulelist tree) → rules
Arguments: tree — Guard (treep tree).
Returns: rules — Type (rulelistp rules).

Definitions and Theorems

Function: abstract-rulelist

(defun abstract-rulelist (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail)) (abstract-fail))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess)))
    (abstract-*-rule-/-*cwsp-cnl trees)))

Theorem: rulelistp-of-abstract-rulelist

(defthm rulelistp-of-abstract-rulelist
  (b* ((rules (abstract-rulelist tree)))
    (rulelistp rules))
  :rule-classes :rewrite)