@@ -86,7 +86,7 @@ number as 0), we could write:
87 fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
87 fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
88 fibonacci {lag} Z = lag
88 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
91After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
91After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
92and will return the 5th fibonacci number. Note that while this works, this is not the
92and will return the 5th fibonacci number. Note that while this works, this is not the