		Search-engine friendly clone of the ACL2 documentation.

Number-theory

Dm::primep

Recognizer of prime numbers.

This is taken from the RTL library.

Function: primep

(defun dm::primep (n)
  (declare (xargs :guard t))
  (and (integerp n)
       (>= n 2)
       (equal (dm::least-divisor 2 n) n)))

Function: least-divisor

(defun dm::least-divisor (k n)
  (declare (xargs :guard t))
  (if (and (integerp n)
           (integerp k)
           (< 1 k)
           (<= k n))
      (if (dm::divides k n)
          k
        (dm::least-divisor (1+ k) n))
    nil))

Function: divides

(defun dm::divides (x y)
  (declare (xargs :guard t))
  (and (acl2-numberp x)
       (not (= x 0))
       (acl2-numberp y)
       (integerp (/ y x))))