• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Community
    • 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
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
          • R1cs
          • Interfaces
          • Sha-2
          • Keccak
          • Kdf
          • Mimc
          • Padding
          • Hmac
          • Elliptic-curves
            • Secp256k1-attachment
            • Twisted-edwards
            • Montgomery
            • Short-weierstrass-curves
            • Birational-montgomery-twisted-edwards
            • Has-square-root?-satisfies-pfield-squarep
            • Secp256k1
            • Secp256k1-domain-parameters
            • Secp256k1-types
              • Secp256k1-priv-key
              • Secp256k1-pub-key
              • Secp256k1-field
              • Secp256k1-point
                • Secp256k1-point-fix
                • Secp256k1-point-equiv
                • Make-secp256k1-point
                • Secp256k1-point->y
                • Secp256k1-point->x
                • Change-secp256k1-point
                  • Secp256k1-pointp
                • Secp256k1-point-to-bytes
                • Secp256k1-point-infinityp
                • Secp256k1-point-generator
              • Pfield-squarep
              • Secp256k1-interface
              • Prime-field-extra-rules
              • Points
            • Attachments
            • Elliptic-curve-digital-signature-algorithm
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Secp256k1-point

    Change-secp256k1-point

    Modifying constructor for secp256k1-point structures.

    Syntax
    (change-secp256k1-point x 
                            [:x <x>] 
                            [:y <y>]) 
    

    This is an often useful alternative to make-secp256k1-point.

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

    (defmacro change-secp256k1-point (x &rest args)
      (std::change-aggregate 'secp256k1-point
                             x args
                             '((:x . secp256k1-point->x)
                               (:y . secp256k1-point->y))
                             'change-secp256k1-point
                             'nil))