		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-point

Make-secp256k1-point

Basic constructor macro for secp256k1-point structures.

Syntax

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

This is the usual way to construct secp256k1-point structures. It simply conses together a structure with the specified fields.

This macro generates a new secp256k1-point structure from scratch. See also change-secp256k1-point, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-secp256k1-point

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

Function: secp256k1-point

(defun secp256k1-point (x y)
  (declare (xargs :guard (and (secp256k1-fieldp x)
                              (secp256k1-fieldp y))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'secp256k1-point))
    (declare (ignorable acl2::__function__))
    (b* ((x (mbe :logic (secp256k1-field-fix x)
                 :exec x))
         (y (mbe :logic (secp256k1-field-fix y)
                 :exec y)))
      (list x y))))