def foo (rec : Nat → Nat → Nat) : Nat → Nat → Nat
| 0     a := a
| (n+1) a := rec n a + a + rec n (a+1)

partial def fix' (f: (Nat → Nat → Nat) → (Nat → Nat → Nat)) : Nat → Nat → Nat
| a b := f fix' a b

def prof {α : Type} (msg : String) (p : IO α) : IO α :=
let msg := "Time for '" ++ msg ++ "':" in
timeit msg p

def fix_test (n : Nat) : IO Unit :=
IO.println (fix foo n 10)

def fix'_test (n : Nat) : IO Unit :=
IO.println (fix' foo n 10)

def main (xs : List String) : IO Unit :=
prof "native fix" (fix_test xs.head.toNat) *>
prof "fix in lean" (fix'_test xs.head.toNat) *>
pure ()