Is it bad form to use default annotation for default arguments?

Viewed 36

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 default annotation. It is included here for illustrative purposes only. Usually, default is 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?

0 Answers
Related