f : (N -> N) -> N * N -> N -> Z
f g (x,y) z = x + g y - z   -- here g y is function application

-- This used to be allowed, but now function application is
-- *syntactically* disambiguated from multiplication.  'g y' must be
-- function application because the left-hand term is a variable.
-- q : ℕ → ℕ×ℕ → ℕ → ℤ
-- q g (x,y) z = x + g y - z    -- here g y is multiplication


||| 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
          is 0
  ,  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.
  ?}

-- Mutually recursive functions.  The order of declarations and
-- definitions does not matter.
isEven : N -> Bool
isOdd  : N -> Bool

-- We can either write a definition explicitly using a case...
isEven n =
  {? true      when n is 0
  ,  isOdd m   when n is m+1
  ?}

-- Or we can directly define by cases like this (which is just syntax
-- sugar for something like the former).
isOdd 0     = false
isOdd (m+1) = isEven m

-- Again, here are two equivalent definitions of fact using the two
-- different styles.

fact : N -> N
fact n =
  {? 1            when n is 0,
     n * fact m   when n is m+1
  ?}

fact2 : N -> N
fact2 0     = 1
fact2 (m+1) = (m + 1) * fact2 m