@@ -14,7 +14,7 @@ In this section we discuss a variety of additional features:
14+ code generation; and
14+ code generation; and
15+ the universe hierarchy.
15+ the universe hierarchy.
17−Auto implicit arguments
17+Implicit arguments
18=======================
18=======================
20We have already seen implicit arguments, which allows arguments to be
20We 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.
23.. code-block:: idris
23.. code-block:: idris
25 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
25 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
27+Auto implicit arguments
28+------------------------
27In other situations, it may be possible to infer arguments not by type
30In other situations, it may be possible to infer arguments not by type
28checking but by searching the context for an appropriate value, or
31checking 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:
66.. code-block:: idris
69.. code-block:: idris
68 head xs {p = ?headProof}
71 head xs {p = ?headProof}
73+Default implicit arguments
74+---------------------------
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:
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)
88+Here, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``.
70Implicit conversions
91Implicit conversions
71====================
92====================