@@ -14,7 +14,7 @@ In this section we discuss a variety of additional features:
1414+ code generation; and
1515+ the universe hierarchy.
1616
17−Auto implicit arguments
17+Implicit arguments
1818=======================
1919
2020We have already seen implicit arguments, which allows arguments to be
@@ -23,6 +23,9 @@ omitted when they can be inferred by the type checker, e.g.
2323.. code-block:: idris
2424
2525 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
26+
27+Auto implicit arguments
28+------------------------
2629
2730In other situations, it may be possible to infer arguments not by type
2831checking but by searching the context for an appropriate value, or
@@ -66,6 +69,30 @@ In the case that a proof is not found, it can be provided explicitly as normal:
6669.. code-block:: idris
6770
6871 head xs {p = ?headProof}
72+
73+Default implicit arguments
74+---------------------------
75+
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:
84+
85+.. code-block:: idris
86+
87+ fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
88+ fibonacci {lag} Z = lag
89+ fibonacci {lag} {lead} (S Z) = fibonacci {lag=lead} {lead=lag+lead} n
90+
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.
95+
6996
7097Implicit conversions
7198====================