@@ -86,7 +86,7 @@ number as 0), we could write:
8686
8787 fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
8888 fibonacci {lag} Z = lag
89− fibonacci {lag} {lead} (S Z) = fibonacci {lag=lead} {lead=lag+lead} n
89+ fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
9090
9191After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
9292and will return the 5th fibonacci number. Note that while this works, this is not the