fib.disco

||| A naive implementation of the fibonacci function.
!!!   fib 0 == 0
!!!   fib 1 == 1
!!!   fib 2 == 1
!!!   fib 5 == 5
!!!   fib 12 == 144
fib : Nat -> Nat                 -- a top-level recursive function
fib n =
  {? n when
        n           -- note how a single branch can be
          is 0      -- broken across multiple lines
  ,  n                  when n is 1  -- comment
  ,  fib (n .- 1) + fib (n .- 2)  otherwise
    -- note we can't write
    --   fib (n-1) + fib (n-2) otherwise
    -- since that doesn't pass the type checker: it doesn't believe
    -- that (n-1) and (n-2) are natural numbers.
  ?}