		Search-engine friendly clone of the ACL2 documentation.

Factorial-cosim

Fact

Signature
(fact n) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: fact

(defun fact (n)
       (declare (xargs :guard (natp n)))
       (let ((__function__ 'fact))
            (declare (ignorable __function__))
            (if (or (< n 2) (not (integerp n)))
                1 (* n (fact (- n 1))))))