• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
      • Fty-extensions
      • Defsubtype
      • Defset
      • Deftypes
      • Specific-types
      • Defflatsum
        • Defflatsum-implementation
          • Defflatsum-fn
          • Defflatsum-theorem
          • Defflatsum-flex-summand
          • Defflatsum-flex-summands
          • Defflatsum-theorems
          • Defflatsum-macro-definition
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defomap
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))))))))))))))))))