		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))))