		Search-engine friendly clone of the ACL2 documentation.

Fibonacci-cosim

Fib

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

Definitions and Theorems

Function: fib

(defun fib (n)
       (declare (xargs :guard (natp n)))
       (declare (xargs :guard (natp n)))
       (let ((__function__ 'fib))
            (declare (ignorable __function__))
            (cond ((zp n) 0)
                  ((eql n 1) 1)
                  (t (+ (fib (- n 1)) (fib (- n 2)))))))