		Search-engine friendly clone of the ACL2 documentation.

Defflatsum-implementation

Defflatsum-theorems

Generate all the theorems associated to the summands.

Signature
(defflatsum-theorems summand-predicates sum-predicate) → thm
Arguments: summand-predicates — Guard (symbol-listp summand-predicates).; sum-predicate — Guard (symbolp sum-predicate).
Returns: thm — A ACL2::pseudo-event-form-listp.

Definitions and Theorems

Function: defflatsum-theorems

(defun defflatsum-theorems (summand-predicates sum-predicate)
  (declare (xargs :guard (and (symbol-listp summand-predicates)
                              (symbolp sum-predicate))))
  (let ((__function__ 'defflatsum-theorems))
    (declare (ignorable __function__))
    (cond ((endp summand-predicates) nil)
          (t (cons (defflatsum-theorem (car summand-predicates)
                                       sum-predicate)
                   (defflatsum-theorems (cdr summand-predicates)
                                        sum-predicate))))))