@@ -73,19 +73,25 @@ In the case that a proof is not found, it can be provided explicitly as normal:
7373Default implicit arguments
7474---------------------------
7575
76−Besides having Idris automatically find any value of a given type, sometimes we
77−want to have an implicit argument with a default value. Idris provides this
78−functionality through the ``default`` annotation. For example, if we want to
79−compute the n'th fibonacci number (and setting the 0'th as 0), we can write:
76+Besides having Idris automatically find a value of a given type, sometimes we
77+want to have an implicit argument with a specific default value. In Idris, we can
78+do this using the ``default`` annotation. While this is primarily intended to assist
79+in automatically constructing a proof where auto fails, or finds an unhelpful value,
80+it might be easier to first consider a simpler case, not involving proofs.
81+
82+If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
83+number as 0), we could write:
8084
8185.. code-block:: idris
8286
83− fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> Nat -> Nat
87+ fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
8488 fibonacci {lag} Z = lag
85− fibonacci {lead} (S Z) = lead
86− fibonacci {lag} {lead} (S (S n)) = fibonacci {lag=lead} {lead=lag+lead} (S n)
89+ fibonacci {lag} {lead} (S Z) = fibonacci {lag=lead} {lead=lag+lead} n
8790
88−Here, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``.
91+After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
92+and will return the 5th fibonacci number. Note that while this works, this is not the
93+intended use of the ``default`` annotation. It is included here for illustrative purposes
94+only. Usually, ``default`` is used to provide things like a custom proof search script.
8995
9096
9197Implicit conversions