@@ -49,11 +49,19 @@ this to happen silently. We define ``head`` as follows:
4949 head (x :: xs) = x
5050
5151The ``auto`` annotation on the implicit argument means that Idris
52−will attempt to fill in the implicit argument using the ``trivial``
53−tactic, which searches through the context for a proof, and tries to
54−solve with ``refl`` if a proof is not found. Now when ``head`` is
55−applied, the proof can be omitted. In the case that a proof is not
56−found, it can be provided explicitly as normal:
52+will attempt to fill in the implicit argument by searching for a value
53+of the appropriate type. It will try the following, in order:
54+
55+- Local variables, i.e. names bound in pattern matches or ``let`` bindings,
56+ with exactly the right type.
57+- The constructors of the required type. If they have arguments, it will
58+ search recursively up to a maximum depth of 100.
59+- Local variables with function types, searching recursively for the
60+ arguments.
61+- Any function with the appropriate return type which is marked with the
62+ ``%hint`` annotation.
63+
64+In the case that a proof is not found, it can be provided explicitly as normal:
5765
5866.. code-block:: idris
5967