• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
              • Atj-java-primitives
              • Atj-java-primitive-arrays
              • Atj-type-macros
              • Atj-java-syntax-operations
              • Atj-fn
              • Atj-library-extensions
              • Atj-java-input-types
              • Atj-test-structures
                • Atj-test-value
                • Atj-test
                  • Atj-test-fix
                  • Make-atj-test
                  • Atj-test-equiv
                  • Change-atj-test
                  • Atj-test->outputs
                  • Atj-test->inputs
                  • Atj-test->function
                  • Atj-test->name
                  • Atj-testp
                • Atj-test-value-of-type
                • Atj-test-values-of-types
                • Atj-test-value-to-type
                • Atj-test-values-to-types
                • Atj-test-value-ACL2-list
                • Atj-test-value-list
                • Atj-test-list
              • Aij-notions
              • Atj-macro-definition
            • Atj-tutorial
          • Aij
          • Language
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Atj-test-structures

Atj-test

Processed user-specified ATJ tests.

This is a product type introduced by fty::defprod.

Fields
name — stringp
function — symbolp
inputs — atj-test-value-list
outputs — atj-test-value-list

Each test specified by the :tests input must have the form (namej termj), where termj must translate to (fn in1 in2 ...), as explained in the documentation. As the :tests input is processed, the information about each test is stored into a value of this product type. This product type stores namej, fn, the list of inputs derived from in1, in2, etc., and results of the ground call (fn in1 in2 ...). The latter list is a singleton for single-valued functions, while it consists of two or more values for multi-valued functions.

Subtopics

Atj-test-fix
Fixing function for atj-test structures.
Make-atj-test
Basic constructor macro for atj-test structures.
Atj-test-equiv
Basic equivalence relation for atj-test structures.
Change-atj-test
Modifying constructor for atj-test structures.
Atj-test->outputs
Get the outputs field from a atj-test.
Atj-test->inputs
Get the inputs field from a atj-test.
Atj-test->function
Get the function field from a atj-test.
Atj-test->name
Get the name field from a atj-test.
Atj-testp
Recognizer for atj-test structures.