		Search-engine friendly clone of the ACL2 documentation.

Dependencies

Flexprod-fields-direct-dependencies

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

Definitions and Theorems

Function: flexprod-fields-direct-dependencies

(defun flexprod-fields-direct-dependencies
       (flexprod-fields fty-table)
 (declare (xargs :guard (and (flexprod-field-listp flexprod-fields)
                             (alistp fty-table))))
 (let ((__function__ 'flexprod-fields-direct-dependencies))
  (declare (ignorable __function__))
  (if
   (consp flexprod-fields)
   (b*
    ((recog (flexprod-field->type (first flexprod-fields)))
     ((unless (symbolp recog))
      (raise "Internal error: malformed type recognizer ~x0."
             recog))
     (name?
          (name-of-flextypes-containing-recognizer recog fty-table))
     (names
         (flexprod-fields-direct-dependencies (rest flexprod-fields)
                                              fty-table)))
    (if (or (not name?) (member-eq name? names))
        names
      (cons name? names)))
   nil)))

Theorem: symbol-listp-of-flexprod-fields-direct-dependencies

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

Theorem: true-listp-of-flexprod-fields-direct-dependencies

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