In the docs, they show how you can use the default annotation to create default arguments, like
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
such that fibonacci 5 is the same as fibonacci {lag=0} {lead=1} 5. They then say
Note that while this works, this is not the intended use of the
defaultannotation. It is included here for illustrative purposes only. Usually,defaultis used to provide things like a custom proof search script.
Is it problematic or bad form to use default to create default arguments like in the fibonacci example? If so, why?