• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • 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-gen-test-method
                • Atj-shallow-code-generation
                • Atj-common-code-generation
                • Atj-shallow-quoted-constant-generation
                  • Atj-qconstants-p
                  • Atj-gen-shallow-symbol
                  • Atj-gen-shallow-cons-field-name
                  • Atj-gen-shallow-symbol-field-name
                  • Atj-add-qconstant
                  • Atj-add-qconstants-in-term
                    • Atj-add-qconstants-in-terms
                  • Atj-gen-shallow-symbol-field
                  • Atj-gen-shallow-rational-id-part
                  • Atj-gen-shallow-number-id-part
                  • Atj-gen-shallow-number-field
                  • Atj-gen-shallow-value
                  • Atj-gen-shallow-cons-fields
                  • Atj-gen-shallow-cons-field
                  • Atj-gen-shallow-string
                  • Atj-gen-shallow-integer-id-part
                  • Atj-gen-shallow-string-field
                  • Atj-gen-shallow-number-field-name
                  • Atj-gen-shallow-char-field
                  • Atj-gen-shallow-char
                  • Atj-gen-shallow-string-field-name
                  • Atj-gen-shallow-cons
                  • Atj-gen-shallow-char-field-name
                  • Atj-gen-shallow-symbol-fields
                  • Atj-gen-shallow-string-fields
                  • Atj-gen-shallow-number-fields
                  • Atj-gen-shallow-number
                  • Atj-gen-shallow-char-fields
                • Atj-pre-translation
                • Atj-gen-everything
                • Atj-name-translation
                • Atj-gen-test-cunit
                • Atj-gen-test-class
                • Atj-gen-main-file
                • Atj-post-translation
                • Atj-deep-code-generation
                • Atj-gen-test-methods
                • Atj-gen-test-file
                • Atj-gen-env-file
                • Atj-gen-output-subdir
              • 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
              • 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-shallow-quoted-constant-generation

Atj-add-qconstants-in-term

Collect all the quoted constants in a term.

Signature
(atj-add-qconstants-in-term term qconsts) → new-qconsts
Arguments
term — Guard (pseudo-termp term).
qconsts — Guard (atj-qconstants-p qconsts).
Returns
new-qconsts — Type (atj-qconstants-p new-qconsts), given (atj-qconstants-p qconsts).

We return all the values of the quoted constants that appear directly quoted in the term. That is, for each sub-term of the form (quote <value>), we return <value>. This excludes value that occur (only) inside other quoted values, e.g. (quote (<value> . ...)).

The record that stores the collected constants is threaded through the recursive functions.

Theorem: return-type-of-atj-add-qconstants-in-term.new-qconsts

(defthm return-type-of-atj-add-qconstants-in-term.new-qconsts
 (implies
      (atj-qconstants-p qconsts)
      (b* ((?new-qconsts (atj-add-qconstants-in-term term qconsts)))
        (atj-qconstants-p new-qconsts)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-add-qconstants-in-terms.new-qconsts

(defthm return-type-of-atj-add-qconstants-in-terms.new-qconsts
 (implies
    (atj-qconstants-p qconsts)
    (b* ((?new-qconsts (atj-add-qconstants-in-terms terms qconsts)))
      (atj-qconstants-p new-qconsts)))
 :rule-classes :rewrite)

Subtopics

Atj-add-qconstants-in-terms