		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Rulelist-incremental-ok-p

Check if incremental rules appear after non-incremental rules with the same names.

Signature
(rulelist-incremental-ok-p rules) → yes/no
Arguments: rules — Guard (rulelistp rules).
Returns: yes/no — Type (booleanp yes/no).

An incremental rule may appear only if there is a preceding rule with the same name. A non-incremental rule may appear only if there is no preceding rule with the same name.

Definitions and Theorems

Function: rulelist-incremental-ok-p-aux

(defun rulelist-incremental-ok-p-aux (previous-rules next-rules)
  (declare (xargs :guard (and (rulelistp previous-rules)
                              (rulelistp next-rules))))
  (or (endp next-rules)
      (and (iff (rule->incremental (car next-rules))
                (lookup-rulename (rule->name (car next-rules))
                                 previous-rules))
           (rulelist-incremental-ok-p-aux
                (append previous-rules (list (car next-rules)))
                (cdr next-rules)))))

Theorem: booleanp-of-rulelist-incremental-ok-p-aux

(defthm booleanp-of-rulelist-incremental-ok-p-aux
  (b*
   ((yes/no
         (rulelist-incremental-ok-p-aux previous-rules next-rules)))
   (booleanp yes/no))
  :rule-classes :rewrite)

Function: rulelist-incremental-ok-p

(defun rulelist-incremental-ok-p (rules)
  (declare (xargs :guard (rulelistp rules)))
  (rulelist-incremental-ok-p-aux nil rules))

Theorem: booleanp-of-rulelist-incremental-ok-p

(defthm booleanp-of-rulelist-incremental-ok-p
  (b* ((yes/no (rulelist-incremental-ok-p rules)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Subtopics

Rulelist-incremental-ok-p-aux: Auxiliary function to define rulelist-incremental-ok-p.