• 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
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
                • Atc-symbolic-computation-states
                • Atc-symbolic-execution-rules
                • Atc-gen-ext-declon-lists
                • Atc-function-and-loop-generation
                • Atc-statement-generation
                • Atc-gen-fileset
                • Atc-gen-everything
                • Atc-gen-obj-declon
                • Atc-gen-fileset-event
                • Atc-tag-tables
                • Atc-expression-generation
                • Atc-generation-contexts
                • Atc-gen-wf-thm
                • Term-checkers-atc
                • Atc-variable-tables
                • Term-checkers-common
                • Atc-gen-init-fun-env-thm
                • Atc-gen-appconds
                • Read-write-variables
                • Atc-gen-thm-assert-events
                • Test*
                • Atc-gen-prog-const
                • Atc-gen-expr-bool
                • Atc-theorem-generation
                • Atc-tag-generation
                • Atc-gen-expr-pure
                • Atc-function-tables
                  • Atc-fn-info
                    • Atc-fn-info-fix
                    • Make-atc-fn-info
                    • Atc-fn-infop
                    • Atc-fn-info-equiv
                    • Change-atc-fn-info
                      • Atc-fn-info->measure-nat-thm
                      • Atc-fn-info->correct-mod-thm
                      • Atc-fn-info->result-thm
                      • Atc-fn-info->out-type
                      • Atc-fn-info->in-types
                      • Atc-fn-info->fun-env-thm
                      • Atc-fn-info->extobjs
                      • Atc-fn-info->correct-thm
                      • Atc-fn-info->loop?
                      • Atc-fn-info->limit
                      • Atc-fn-info->guard
                      • Atc-fn-info->affect
                    • Atc-symbol-fninfo-alist-to-result-thms
                    • Atc-symbol-fninfo-alist-to-measure-nat-thms
                    • Atc-symbol-fninfo-alist-to-fun-env-thms
                    • Atc-symbol-fninfo-alist-to-correct-thms
                    • Atc-symbol-fninfo-alist
                  • Atc-object-tables
                • Fty-pseudo-term-utilities
                • Atc-term-recognizers
                • Atc-input-processing
                • Atc-shallow-embedding
                • Atc-process-inputs-and-gen-everything
                • Atc-table
                • Atc-fn
                • Atc-pretty-printing-options
                • Atc-types
                • Atc-macro-definition
              • Atc-tutorial
            • Language
            • Representation
            • Transformation-tools
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • 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
    • Atc-fn-info

    Change-atc-fn-info

    Modifying constructor for atc-fn-info structures.

    Syntax
    (change-atc-fn-info x 
                        [:out-type <out-type>] 
                        [:in-types <in-types>] 
                        [:loop? <loop?>] 
                        [:affect <affect>] 
                        [:extobjs <extobjs>] 
                        [:result-thm <result-thm>] 
                        [:correct-thm <correct-thm>] 
                        [:correct-mod-thm <correct-mod-thm>] 
                        [:measure-nat-thm <measure-nat-thm>] 
                        [:fun-env-thm <fun-env-thm>] 
                        [:limit <limit>] 
                        [:guard <guard>]) 
    

    This is an often useful alternative to make-atc-fn-info.

    We construct a new atc-fn-info structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

    Definition

    This is an ordinary change- macro introduced by fty::defprod.

    Macro: change-atc-fn-info

    (defmacro change-atc-fn-info (x &rest args)
      (std::change-aggregate
           'atc-fn-info
           x args
           '((:out-type . atc-fn-info->out-type)
             (:in-types . atc-fn-info->in-types)
             (:loop? . atc-fn-info->loop?)
             (:affect . atc-fn-info->affect)
             (:extobjs . atc-fn-info->extobjs)
             (:result-thm . atc-fn-info->result-thm)
             (:correct-thm . atc-fn-info->correct-thm)
             (:correct-mod-thm . atc-fn-info->correct-mod-thm)
             (:measure-nat-thm . atc-fn-info->measure-nat-thm)
             (:fun-env-thm . atc-fn-info->fun-env-thm)
             (:limit . atc-fn-info->limit)
             (:guard . atc-fn-info->guard))
           'change-atc-fn-info
           'nil))