		Search-engine friendly clone of the ACL2 documentation.

Points

Pointp

Recognize all possible points of all possible elliptic curves.

Signature
(pointp point) → *

This models (at least) all possible points of all possible elliptic curves. A point, as modeled here, is either a pair of natural numbers or a special point at infinity.

This type of points is perhaps more general then elliptic curves, and thus it might be factored out into some more general library.

Definitions and Theorems

Function: pointp

(defun pointp (point)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'pointp))
    (declare (ignorable acl2::__function__))
    (or (and (consp point)
             (natp (car point))
             (natp (cdr point)))
        (eq point :infinity))))