		Search-engine friendly clone of the ACL2 documentation.

Points-fty

Point-kind

Kinds (i.e. tags) of elliptic curve points.

Signature
(point-kind p) → kind
Arguments: p — Guard (pointp p).
Returns: kind — Type (keywordp kind).

Definitions and Theorems

Function: point-kind

(defun point-kind (p)
  (declare (xargs :guard (pointp p)))
  (let ((acl2::__function__ 'point-kind))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (and (pointp p) (consp p))
             :finite
           :infinite)
         :exec (if (consp p) :finite :infinite))))

Theorem: keywordp-of-point-kind

(defthm keywordp-of-point-kind
  (b* ((kind (point-kind p)))
    (keywordp kind))
  :rule-classes :rewrite)

Theorem: point-kind-of-point-fix-p

(defthm point-kind-of-point-fix-p
  (equal (point-kind (point-fix p))
         (point-kind p)))

Theorem: point-kind-point-equiv-congruence-on-p

(defthm point-kind-point-equiv-congruence-on-p
  (implies (point-equiv p p-equiv)
           (equal (point-kind p)
                  (point-kind p-equiv)))
  :rule-classes :congruence)

Theorem: point-kind-possibilities

(defthm point-kind-possibilities
  (or (equal (point-kind p) :finite)
      (equal (point-kind p) :infinite))
  :rule-classes
  ((:forward-chaining :trigger-terms ((point-kind p)))))