		Search-engine friendly clone of the ACL2 documentation.

Defflatsum-implementation

Defflatsum-flex-summands

Generate all the summands of the defflexsum.

Signature
(defflatsum-flex-summands flat-summands wrld) → (mv flex-summands predicates fixers)
Arguments: flat-summands — Guard (true-listp flat-summands).; wrld — Guard (plist-worldp wrld).

Suitably set the flag that says whether the summand is the last one.

Definitions and Theorems

Function: defflatsum-flex-summands

(defun defflatsum-flex-summands (flat-summands wrld)
  (declare (xargs :guard (and (true-listp flat-summands)
                              (plist-worldp wrld))))
  (let ((__function__ 'defflatsum-flex-summands))
    (declare (ignorable __function__))
    (b* (((when (endp flat-summands))
          (mv nil nil nil))
         ((mv flex-summand predicate fixer)
          (defflatsum-flex-summand (car flat-summands)
                                   (endp (cdr flat-summands))
                                   wrld))
         ((mv flex-summands predicates fixers)
          (defflatsum-flex-summands (cdr flat-summands)
                                    wrld)))
      (mv (cons flex-summand flex-summands)
          (cons predicate predicates)
          (cons fixer fixers)))))