• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixequiv
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
        • Deffold-reduce
          • Deffold-reduce-implementation
            • Deffold-reduce-event-generation
            • Deffoldred-process-inputs-and-gen-everything
            • Deffoldred-fn
            • Deffold-reduce-input-processing
              • Deffoldred-process-inputs
              • Deffoldred-process-override
              • Deffoldred-process-types
              • *deffoldred-allowed-options*
            • Deffoldred-macro-definition
        • Deffold-map
        • Defmake-self
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defomap
      • Defbytelist
      • Fty::basetypes
      • 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

• Deffold-reduce-implementation

Deffold-reduce-input-processing

Input processing performed by deffold-reduce.

See input processing for general background.

Subtopics

Deffoldred-process-inputs

Process all the inputs.

Deffoldred-process-override

Process the :override input.

Deffoldred-process-types

Process the :types input.

*deffoldred-allowed-options*

Keyword options accepted by deffold-reduce.