• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • C
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Ethereum
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Zcash
      • Des
      • X86isa
      • Sha-2
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
            • Escape
            • Swcase-list->value-list
            • Hex-digit-list->chars
            • Fundef-list->name-list
            • Literal
            • Path
            • Hex-string-rest-element
            • Plain-string
            • String-element
            • Hex-string-content-option
            • Hex-string-content
            • Identifier
            • Funcall-option
            • Expression-option
            • Statement-option
            • Literal-option
            • Identifier-option
            • Hex-string
            • Hex-quad
            • Hex-digit
            • Hex-pair
            • Data-value
            • Data-item
            • Statements-to-fundefs
            • String-element-list-result
              • String-element-list-result-fix
              • String-element-list-result-equiv
              • String-element-list-result-ok
                • String-element-list-result-ok->get
                • Make-string-element-list-result-ok
                • Change-string-element-list-result-ok
                • String-element-list-result-err
                • String-element-list-resultp
                • String-element-list-result-kind
              • Identifier-identifier-map-result
              • Swcase-result
              • String-element-result
              • Statement-result
              • Literal-result
              • Identifier-set-result
              • Identifier-result
              • Identifier-list-result
              • Fundef-result
              • Funcall-result
              • Expression-result
              • Escape-result
              • Path-result
              • Block-result
              • Objects
              • Statements/blocks/cases/fundefs
              • Identifier-list
              • Identifier-set
              • Identifier-identifier-map
              • Identifier-identifier-alist
              • Hex-string-rest-element-list
              • String-element-list
              • Path-list
              • Hex-digit-list
              • Literal-list
              • Fundef-list
              • Expressions/funcalls
              • Abstract-syntax-induction-schemas
            • Dynamic-semantics
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
            • Errors
          • Yul-json
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Axe
        • Poseidon
        • Where-do-i-place-my-book
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • String-element-list-result-ok

    Change-string-element-list-result-ok

    Modifying constructor for string-element-list-result-ok structures.

    Syntax
    (change-string-element-list-result-ok x 
                                          [:get <get>]) 
    

    This is an often useful alternative to make-string-element-list-result-ok.

    We construct a new string-element-list-result-ok 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-string-element-list-result-ok

    (defmacro change-string-element-list-result-ok (x &rest args)
      (std::change-aggregate
           'string-element-list-result-ok
           x args
           '((:get . string-element-list-result-ok->get))
           'change-string-element-list-result-ok
           'nil))