@@ -240,6 +240,74 @@ which is trivially provable using reflexivity:
240240 rewriteWith (Var `{{ih}})
241241 reflexivity)
242242
243−Again, we can cut & paste this into the hole in the original file.
243+We can't just cut & paste this into the hole in the original file like this:
244+
245+.. code-block:: idris
246+
247+ import Pruviloj
248+ import Pruviloj.Induction
249+
250+ %language ElabReflection
251+
252+ plusReducesZ' : (n:Nat) -> n = plus n Z
253+ plusReducesZ' Z = %runElab (do reflexivity)
254+ plusReducesZ' (S k) = let ih = plusReducesZ' k in
255+ (%runElab (do intro `{{k}}
256+ intro `{{ih}}
257+ rewriteWith (Var `{{ih}})
258+ reflexivity)
259+ )
260+
261+because this gives the following error:
262+
263+.. code-block:: idris
264+
265+ Idris> :load elabInteractiveEx2.idr
266+ elabInteractiveEx2.idr:10:32:
267+ |
268+ 10 | intro `{{ih}}
269+ | ^
270+ unexpected "in"
271+ expecting dependent type signature
272+
273+We can try putting the proof into a seperate function like this:
274+
275+.. code-block:: idris
276+
277+ import Pruviloj
278+ import Pruviloj.Induction
279+
280+ %language ElabReflection
281+
282+ plusredZ_S : (n : Nat) -> (n = plus n Z) -> (S n = S (plus n Z))
283+ plusredZ_S k ih = %runElab (do intro `{{k}}
284+ intro `{{ih}}
285+ rewriteWith (Var `{{ih}})
286+ reflexivity)
287+
288+ plusReducesZ' : (n:Nat) -> n = plus n Z
289+ plusReducesZ' Z = %runElab (do reflexivity)
290+ plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih
291+
292+but this gives:
293+
294+.. code-block:: idris
295+
296+ Idris> :load elabInteractiveEx4.idr
297+ Type checking ./elabInteractiveEx4.idr
298+ elabInteractiveEx4.idr:7:19-10:43:
299+ |
300+ 7 | plusredZ_S k ih = %runElab (do intro `{{k}}
301+ | ~~~~~~~~~~~~~~~~~~~~~~~~~ ...
302+ When checking right hand side of plusredZ_S with expected type
303+ S k = S (plus k 0)
304+
305+ Can't use lambda here: type is S k = S (plus k 0)
306+
307+ Holes: Main.plusredZ_S
308+
309+Issues like this are discussed here [#f1]_
310+
311+.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556
244312
245313.. |image| image:: ../image/plusReducesProof.png