		Search-engine friendly clone of the ACL2 documentation.

Defflatsum-implementation

Defflatsum-fn

Generate the defflexsum.

Signature
(defflatsum-fn args wrld) → event
Arguments: args — Guard (true-listp args).; wrld — Guard (plist-worldp wrld).
Returns: event — A ACL2::pseudo-event-formp.

Definitions and Theorems

Function: defflatsum-fn

(defun defflatsum-fn (args wrld)
 (declare (xargs :guard (and (true-listp args)
                             (plist-worldp wrld))))
 (let ((__function__ 'defflatsum-fn))
  (declare (ignorable __function__))
  (b*
   ((allowed-keywords '(:pred :fix :equiv
                              :parents :short
                              :long :prepwork))
    ((mv options type+summands)
     (extract-keywords 'defflatsum
                       allowed-keywords args nil))
    ((cons type flat-summands)
     type+summands)
    (pred (getarg :pred (add-suffix-to-fn type "-P")
                  options))
    (fix (getarg :fix (add-suffix-to-fn type "-FIX")
                 options))
    (equiv (getarg :equiv (add-suffix-to-fn type "-EQUIV")
                   options))
    (parents (getarg :parents :noparents options))
    (short (getarg :short nil options))
    (long (getarg :long nil options))
    ((mv flex-summands predicates fixers)
     (defflatsum-flex-summands flat-summands wrld))
    (default-prepwork
     (cons (cons 'local
                 (cons (cons 'in-theory
                             (cons (cons 'enable
                                         (append predicates fixers))
                                   'nil))
                       'nil))
           'nil))
    (prepwork (getarg :prepwork default-prepwork options))
    (theorems (defflatsum-theorems predicates pred)))
   (cons
    'defflexsum
    (cons
     type
     (append
      (and (not (eq parents :noparents))
           (list :parents parents))
      (append
       (and short (list :short short))
       (append
        (and long (list :long long))
        (append
         flex-summands
         (cons
          ':pred
          (cons
           pred
           (cons
            ':fix
            (cons
             fix
             (cons
              ':equiv
              (cons
                   equiv
                   (cons ':prepwork
                         (cons prepwork
                               (cons '/// theorems))))))))))))))))))