		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-cliques-folds

Generate fold functions, or fold function cliques, for a list of type cliques with given names.

Signature
(deffoldred-gen-cliques-folds clique-names suffix targets extra-args result default combine overrides fty-table) → events
Arguments: clique-names — Guard (symbol-listp clique-names).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; result — Guard (symbolp result).; combine — Guard (symbolp combine).; overrides — Guard (alistp overrides).; fty-table — Guard (alistp fty-table).
Returns: events — Type (acl2::pseudo-event-form-listp events).

Definitions and Theorems

Function: deffoldred-gen-cliques-folds

(defun deffoldred-gen-cliques-folds
       (clique-names suffix targets extra-args result
                     default combine overrides fty-table)
  (declare (xargs :guard (and (symbol-listp clique-names)
                              (symbolp suffix)
                              (symbol-listp targets)
                              (true-listp extra-args)
                              (symbolp result)
                              (symbolp combine)
                              (alistp overrides)
                              (alistp fty-table))))
  (let ((__function__ 'deffoldred-gen-cliques-folds))
    (declare (ignorable __function__))
    (b* (((when (endp clique-names)) nil)
         (clique-name (car clique-names))
         (clique (flextypes-with-name clique-name fty-table))
         ((unless clique)
          (raise "Internal error: no type clique with name ~x0."
                 clique-name))
         ((unless (flextypes-p clique))
          (raise "Internal error: malformed type clique ~x0."
                 clique))
         (events (deffoldred-gen-clique-fold/folds
                      clique suffix targets extra-args result
                      default combine overrides fty-table))
         (more-events (deffoldred-gen-cliques-folds
                           (cdr clique-names)
                           suffix targets extra-args result
                           default combine overrides fty-table)))
      (append events more-events))))

Theorem: pseudo-event-form-listp-of-deffoldred-gen-cliques-folds

(defthm pseudo-event-form-listp-of-deffoldred-gen-cliques-folds
  (b* ((events (deffoldred-gen-cliques-folds
                    clique-names
                    suffix targets extra-args result
                    default combine overrides fty-table)))
    (acl2::pseudo-event-form-listp events))
  :rule-classes :rewrite)