• 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
                  • Jbinopp
                  • Jbinop-fix
                  • Jbinop-case
                  • Jbinop-kind
                  • Jbinop-equiv
                  • Jbinop-add
                  • Jbinop-sub
                  • Jbinop-xor
                  • Jbinop-ushr
                  • Jbinop-sshr
                    • Make-jbinop-sshr
                    • Change-jbinop-sshr
                    • Jbinop-shl
                    • Jbinop-rem
                    • Jbinop-ne
                    • Jbinop-mul
                    • Jbinop-lt
                    • Jbinop-le
                    • Jbinop-ior
                    • Jbinop-gt
                    • Jbinop-ge
                    • Jbinop-eq
                    • Jbinop-div
                    • Jbinop-condor
                    • Jbinop-condand
                    • Jbinop-asg-xor
                    • Jbinop-asg-ushr
                    • Jbinop-asg-sub
                    • Jbinop-asg-sshr
                    • Jbinop-asg-shl
                    • Jbinop-asg-rem
                    • Jbinop-asg-mul
                    • Jbinop-asg-ior
                    • Jbinop-asg-div
                    • Jbinop-asg-and
                    • Jbinop-asg-add
                    • Jbinop-asg
                    • Jbinop-and
                  • Jmethod
                  • 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
    • Jbinop-sshr

    Change-jbinop-sshr

    Modifying constructor for jbinop-sshr structures.

    Syntax
    (change-jbinop-sshr x 
                        ) 
    

    This is an often useful alternative to make-jbinop-sshr.

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

    (defmacro change-jbinop-sshr (x &rest args)
      (std::change-aggregate 'jbinop-sshr
                             x args 'nil
                             'change-jbinop-sshr
                             'nil))