• 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

    Show-io-pairs

    Display verified input-output pairs

    See add-io-pairs for relevant background. Show-io-pairs prints I/O pairs in a pleasant format, each starting on a new line. It is evaluated only for its side effect of printing. See get-io-pairs for a related utility, which returns a list of evaluated I/O pairs.

    Show-io-pairs displays all (verified) I/O pairs for the specified function symbols. Normally printing goes to the terminal, but more generally it goes to standard-co.

    General Forms:
    (show-io-pairs :all)
    (show-io-pairs) ; same as above
    (show-io-pairs fn1 ... fnk) ; k > 0

    where the arguments are not evaluated. If no arguments are supplied, or equivalently there is a single argument, :all, then all I/O pairs are to be printed; otherwise, all I/O pairs are printed only for the specified function symbols.

    Each I/O pair is printed in the format expected as input to add-io-pairs, that is, the inputs and result are terms. In other words, add-io-pairs prints I/O pairs, not evaluated I/O pairs (again, see add-io-pairs for relevant background). Moreover, show-io-pairs displays the inputs and result as quoted terms, such as 'abc, even when they result from a call of add-io-pairs in which the terms were not all quoted, e.g., (car '(abc def)).

    A warning is printed for each fni that has no associated I/O pairs.