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