• 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
                • Jbinop
                • Jmethod
                  • Jmethodp
                  • Jmethod-fix
                  • Make-jmethod
                  • Jmethod-equiv
                  • Change-jmethod
                    • Jmethod->synchronized?
                    • Jmethod->strictfp?
                    • Jmethod->abstract?
                    • Jmethod->throws
                    • Jmethod->static?
                    • Jmethod->result
                    • Jmethod->params
                    • Jmethod->native?
                    • Jmethod->name
                    • Jmethod->final?
                    • Jmethod->body
                    • Jmethod->access
                  • Jtype
                  • Jfield
                  • Jexprs
                  • Jliteral
                  • Junop
                  • Jlocvar
                  • Jcunit
                  • Jaccess
                  • Maybe-jexpr
                  • Jparam
                  • Jimport
                  • Jcinitializer
                  • Jresult
                  • Jstatems+jblocks
                  • Jexpr-get-field
                  • Jliteral-long-dec-nouscores
                  • Nat-to-dec-chars-theorems
                  • Jmethods-to-jcbody-elements
                  • Jclasses-to-jcbody-elements
                  • Jblock-locvar-final
                  • Jblock-locvar
                  • Jliteral-int-dec-nouscores
                  • Jfields-to-jcbody-elements
                  • Jblock-for
                  • Jblock-smethod
                  • Jblock-imethod
                  • Jblock-ifelse
                  • Jblock-asg-name
                  • Jparam-list->types
                  • Jparam-list->names
                  • Jexpr-lit-long-dec-nouscores
                  • Jexpr-lit-int-dec-nouscores
                  • Jexpr-literal-string
                  • Jexpr-literal-floating
                  • Jexpr-literal-character
                  • Jblock-while
                  • Jblock-method
                  • Jblock-if
                  • Jblock-expr
                  • Jblock-do
                  • Jblock-asg
                  • Jexpr-name-list
                  • Jblock-throw
                  • Jblock-return
                  • Jparam-list
                  • Jimport-list
                  • Jexpr-literal-true
                  • Jexpr-literal-null
                  • Jexpr-literal-false
                  • Jexpr-literal-1
                  • Jexpr-literal-0
                  • Jclass-list
                  • Jblock-continue
                  • Jtype-short
                  • Jtype-long
                  • Jtype-list
                  • Jtype-int
                  • Jtype-float
                  • Jtype-double
                  • Jtype-char
                  • Jtype-byte
                  • Jtype-boolean
                  • Jmethod-list
                  • Jliteral-list
                  • Jfield-list
                  • Jblock-list
                  • Jblock-break
                  • Jclasses+jcmembers
                • 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
                • 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
    • Jmethod

    Change-jmethod

    Modifying constructor for jmethod structures.

    Syntax
    (change-jmethod x 
                    [:access <access>] 
                    [:abstract? <abstract?>] 
                    [:static? <static?>] 
                    [:final? <final?>] 
                    [:synchronized? <synchronized?>] 
                    [:native? <native?>] 
                    [:strictfp? <strictfp?>] 
                    [:result <result>] 
                    [:name <name>] 
                    [:params <params>] 
                    [:throws <throws>] 
                    [:body <body>]) 
    

    This is an often useful alternative to make-jmethod.

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

    (defmacro change-jmethod (x &rest args)
      (std::change-aggregate 'jmethod
                             x args
                             '((:access . jmethod->access)
                               (:abstract? . jmethod->abstract?)
                               (:static? . jmethod->static?)
                               (:final? . jmethod->final?)
                               (:synchronized? . jmethod->synchronized?)
                               (:native? . jmethod->native?)
                               (:strictfp? . jmethod->strictfp?)
                               (:result . jmethod->result)
                               (:name . jmethod->name)
                               (:params . jmethod->params)
                               (:throws . jmethod->throws)
                               (:body . jmethod->body))
                             'change-jmethod
                             'nil))