		Search-engine friendly clone of the ACL2 documentation.

Defflatsum-implementation

Defflatsum-flex-summand

Generate a summand of the defflexsum.

Signature
(defflatsum-flex-summand flat-summand lastp wrld) → (mv flex-summand predicate fixer)
Arguments: lastp — Guard (booleanp lastp).; wrld — Guard (plist-worldp wrld).

If (and only if) the summand is the last one, do not generate the :cond part of the summand, because this summand applies when the :conds of the preceding summand do not hold.

Definitions and Theorems

Function: defflatsum-flex-summand

(defun defflatsum-flex-summand (flat-summand lastp wrld)
 (declare (xargs :guard (and (booleanp lastp)
                             (plist-worldp wrld))))
 (let ((__function__ 'defflatsum-flex-summand))
  (declare (ignorable __function__))
  (b*
   ((keyword (first flat-summand))
    (type (second flat-summand))
    (fty-table (get-fixtypes-alist wrld))
    (fty-info (find-fixtype type fty-table))
    (predicate (fixtype->pred fty-info))
    (fixer (fixtype->fix fty-info))
    (flex-summand
     (cons
      keyword
      (cons
       ':fields
       (cons
           (cons (cons 'get
                       (cons ':type
                             (cons type '(:acc-body x))))
                 'nil)
           (cons ':ctor-body
                 (cons 'get
                       (and (not lastp)
                            (list :cond (list predicate 'x))))))))))
   (mv flex-summand predicate fixer))))