		Search-engine friendly clone of the ACL2 documentation.

Points-fty

Point-infinite

Build the elliptic curve point at infinity.

Signature
(point-infinite) → p
Returns: p — Type (pointp p).

Definitions and Theorems

Function: point-infinite

(defun point-infinite nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'point-infinite))
    (declare (ignorable acl2::__function__))
    ':infinity))

Theorem: pointp-of-point-infinite

(defthm pointp-of-point-infinite
  (b* ((p (point-infinite))) (pointp p))
  :rule-classes :rewrite)

Theorem: point-kind-of-point-infinite

(defthm point-kind-of-point-infinite
  (equal (point-kind (point-infinite))
         :infinite))

Theorem: point-fix-when-infinite

(defthm point-fix-when-infinite
  (implies (equal (point-kind p) :infinite)
           (equal (point-fix p) (point-infinite))))

Theorem: equal-of-point-infinite

(defthm equal-of-point-infinite
  (equal (equal (point-infinite) p)
         (and (pointp p)
              (equal (point-kind p) :infinite))))