• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixtype
      • Deffixequiv
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defflatsum
        • Defflatsum-implementation
          • Defflatsum-fn
          • Defflatsum-theorem
          • Defflatsum-flex-summand
          • Defflatsum-flex-summands
          • Defflatsum-theorems
          • Defflatsum-macro-definition
      • Deflist-of-len
      • Defbytelist
      • Defset
      • Specific-types
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Defomap
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Std/util
    • Apt
    • 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
  • Testing-utilities
  • Math

• Defflatsum

Defflatsum-implementation

Implementation of defflatsum.

Subtopics

Defflatsum-fn

Generate the defflexsum.

Defflatsum-theorem

Generate the theorem associated to a summand.

Defflatsum-flex-summand

Generate a summand of the defflexsum.

Defflatsum-flex-summands

Generate all the summands of the defflexsum.

Defflatsum-theorems

Generate all the theorems associated to the summands.

Defflatsum-macro-definition

Definition of the defflatsum macro.