@@ -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,30 @@ 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 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.
82+If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
83+number as 0), we could write:
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
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.
70Implicit conversions
97Implicit conversions
71====================
98====================