git.iko.soy/Idris-dev
on master help sign in
extend holes example
eda6a87martinbaker
docs/proofs/holes.rst+20−1
compare with master
unifiedsplit
@@ -81,10 +81,29 @@ So we are looking for a hole of type Nat and all we know is it has type Nat.
81
81
82Going back to the full term, the above is wrapped in a guess, so it means: 'a guess that is itself a hole'.
82Going back to the full term, the above is wrapped in a guess, so it means: 'a guess that is itself a hole'.
83
83
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+
84Example Showing Patterns
103Example Showing Patterns
85------------------------
104------------------------
86
105
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:
88
107
89.. code-block:: idris
108.. code-block:: idris
90
109