		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-point

Secp256k1-pointp

Recognizer for secp256k1-point structures.

Signature
(secp256k1-pointp p) → *

Definitions and Theorems

Function: secp256k1-pointp

(defun secp256k1-pointp (p)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'secp256k1-pointp))
    (declare (ignorable acl2::__function__))
    (and (true-listp p)
         (eql (len p) 2)
         (b* ((x (std::da-nth 0 p))
              (y (std::da-nth 1 p)))
           (and (secp256k1-fieldp x)
                (secp256k1-fieldp y))))))

Theorem: consp-when-secp256k1-pointp

(defthm consp-when-secp256k1-pointp
  (implies (secp256k1-pointp p) (consp p))
  :rule-classes :compound-recognizer)