		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-r

The prime number that is the order of the large subgroup of Edwards-BLS12.

Signature
(edwards-bls12-r) → r
Returns: r — Type (natp r).

Definitions and Theorems

Function: edwards-bls12-r

(defun edwards-bls12-r nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'edwards-bls12-r))
    (declare (ignorable acl2::__function__))
    (primes::edwards-bls12-subgroup-prime)))

Theorem: natp-of-edwards-bls12-r

(defthm natp-of-edwards-bls12-r
  (b* ((r (edwards-bls12-r))) (natp r))
  :rule-classes :rewrite)

Theorem: primep-of-edwards-bls12-r

(defthm primep-of-edwards-bls12-r
  (dm::primep (edwards-bls12-r)))