		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 (dm::n)
  (declare (xargs :guard t))
  (and (integerp dm::n)
       (>= dm::n 2)
       (equal (dm::least-divisor 2 dm::n)
              dm::n)))

Function: least-divisor

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

Function: divides

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