		Search-engine friendly clone of the ACL2 documentation.

Fibonacci32-cosim

Fib32

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

Definitions and Theorems

Function: fib32

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