• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
          • Add-io-pairs-details
          • Show-io-pairs
          • Get-io-pairs
          • Merge-io-pairs
            • Remove-io-pairs
            • Add-io-pair
            • Deinstall-io-pairs
            • Install-io-pairs
          • Defalist
          • Defmapappend
          • Returns-specifiers
          • Defarbrec
          • Define-sk
          • Defines
          • Error-value-tuples
          • Defmax-nat
          • Defmin-int
          • Deftutorial
          • Extended-formals
          • Defrule
          • Defval
          • Defsurj
          • Defiso
          • Defconstrained-recognizer
          • Deffixer
          • Defmvtypes
          • Defconsts
          • Defthm-unsigned-byte-p
          • Support
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Add-io-pairs

    Merge-io-pairs

    Incorporate I/O pairs from different sources

    General Forms:
    (merge-io-pairs fn event_1 ... event_n)
    (merge-io-pairs (fn_1 ... fn_k) event_1 ... event_n)

    where fn and each fn_i are symbols and each event_i is an event form.

    Example Forms:
    (merge-io-pairs f (include-book "my-book"))
    (merge-io-pairs (f g h) (include-book "book1") (include-book "book2"))

    The second General Form above, (merge-io-pairs (fn_1 ... fn_k) event_1 ... event_n), has an effect equivalent to iterating the first general form as follows.

    (merge-io-pairs fn_1
     (merge-io-pairs fn_2
      ...
      (merge-io-pairs fn_{k-1}
       (merge-io-pairs fn_k event_1 ... event_n))))

    So we focus below on the first General Form.

    Normally you will use merge-io-pairs when an error occurs in add-io-pairs while including a book; see Remark 5 of the documentation for add-io-pairs for explanation. In short: by wrapping (merge-io-pairs fn ...) around one or more include-book events, as illustrated in the Example Forms above, you allow all add-io-pairs forms in the books to complete in a manner that merges together all the I/O pairs for fn.