@@ -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,24 @@ 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 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:
80+
81+.. code-block:: idris
82+
83+ fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> Nat -> Nat
84+ 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)
87+
88+Here, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``.
89+
6990
7091Implicit conversions
7192====================