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