• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
          • Command-error
          • Sign
          • Init-from-mnemonic
          • Command-error-message
          • Stat
            • Stat-fix
            • Stat-equiv
            • Statp
            • Make-stat
            • Stat->keys
            • Stat->addresses
            • Change-stat
            • Next-key
            • Init-from-entropy
            • Process-command
            • Transaction-message
            • Maybe-command-error
            • Maybe-stat
            • Check-stat-file-present
            • Valid-key-path-p
            • String-to-byte-list
            • Load-stat
            • Mnemonic-message
            • Process-sign
            • Process-init-from-entropy
            • All-valid-key-paths-p
            • String-to-word
            • String-to-nat
            • Process-next-key
            • Wallet
            • Process-init-from-mnemonic
            • Check-stat-file-absent
            • Stat-wfp
            • Save-stat
            • Stat-addresses-bounded-p
            • Stat-all-valid-key-paths-p
            • Stat-priv-keys-p
            • Stat-root-depth-zero-p
            • Stat-path-prefix-in-tree-p
            • Crypto-hdwallet-executable
            • *stat-filepath*
            • *key-path-prefix*
            • *coin-type-index*
            • *purpose-index*
            • *external-chain-index*
            • *command-name-init-from-mnemonic*
            • *command-name-init-from-entropy*
            • *account-index*
            • *command-name-sign*
            • *command-name-next-key*
          • Apt
          • Error-checking
          • Fty-extensions
          • Isar
          • Kestrel-utilities
          • Set
          • Soft
          • C
          • 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
    • Stat

    Change-stat

    Modifying constructor for stat structures.

    Syntax
    (change-stat x 
                 [:keys <keys>] 
                 [:addresses <addresses>]) 
    

    This is an often useful alternative to make-stat.

    We construct a new stat 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-stat

    (defmacro change-stat (x &rest args)
      (std::change-aggregate 'stat
                             x args
                             '((:keys . stat->keys)
                               (:addresses . stat->addresses))
                             'change-stat
                             'nil))