@@ -81,10 +81,29 @@ So we are looking for a hole of type Nat and all we know is it has type Nat.
8181
8282Going back to the full term, the above is wrapped in a guess, so it means: 'a guess that is itself a hole'.
8383
84+Since the elaborator does not have any further information it has to be given a value:
85+
86+.. code-block:: idris
87+
88+ %language ElabReflection
89+
90+ testFn : Nat
91+ testFn = %runElab (do fill `(Z)
92+ debug {a = ()}
93+ solve)
94+
95+Now we have a guess for hole_2 which is itself a guess for hole_0:
96+
97+.. code-block:: idris
98+
99+ ?{hole_0} ≈ ?{hole_2} ≈ Prelude.Nat.Z . {hole_2} . {hole_0}
100+
101+The guesses can be accepted by calling the 'solve' tactic.
102+
84103Example Showing Patterns
85104------------------------
86105
87−In this example a parameter 'n' has been added to the function. This allows us to see how patterns are used. Starting with this file:
106+In this next example a parameter 'n' has been added to the function. This allows us to see how patterns are used. Starting with this file:
88107
89108.. code-block:: idris
90109