		Search-engine friendly clone of the ACL2 documentation.

Dependencies

Flexprods-direct-dependencies

Signature
(flexprods-direct-dependencies flexprods fty-table) → dependencies
Arguments: flexprods — Guard (flexprod-listp flexprods).; fty-table — Guard (alistp fty-table).
Returns: dependencies — Type (symbol-listp dependencies).

Definitions and Theorems

Function: flexprods-direct-dependencies

(defun flexprods-direct-dependencies (flexprods fty-table)
 (declare (xargs :guard (and (flexprod-listp flexprods)
                             (alistp fty-table))))
 (let ((__function__ 'flexprods-direct-dependencies))
  (declare (ignorable __function__))
  (if
   (consp flexprods)
   (b* ((fields (flexprod->fields (first flexprods)))
        ((unless (flexprod-field-listp fields))
         (raise "Internal error: malformed flexprod field list ~x0."
                fields)))
    (union-eq (flexprod-fields-direct-dependencies fields fty-table)
              (flexprods-direct-dependencies (rest flexprods)
                                             fty-table)))
   nil)))

Theorem: symbol-listp-of-flexprods-direct-dependencies

(defthm symbol-listp-of-flexprods-direct-dependencies
  (b* ((dependencies
            (flexprods-direct-dependencies flexprods fty-table)))
    (symbol-listp dependencies))
  :rule-classes :rewrite)

Theorem: true-listp-of-flexprods-direct-dependencies

(defthm true-listp-of-flexprods-direct-dependencies
  (b* ((dependencies
            (flexprods-direct-dependencies flexprods fty-table)))
    (true-listp dependencies))
  :rule-classes :type-prescription)