@@ -240,6 +240,74 @@ which is trivially provable using reflexivity:
240 rewriteWith (Var `{{ih}})
240 rewriteWith (Var `{{ih}})
241 reflexivity)
241 reflexivity)
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:
245+.. code-block:: idris
248+ import Pruviloj.Induction
250+ %language ElabReflection
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}}
257+ rewriteWith (Var `{{ih}})
261+because this gives the following error:
263+.. code-block:: idris
265+ Idris> :load elabInteractiveEx2.idr
266+ elabInteractiveEx2.idr:10:32:
271+ expecting dependent type signature
273+We can try putting the proof into a seperate function like this:
275+.. code-block:: idris
278+ import Pruviloj.Induction
280+ %language ElabReflection
282+ plusredZ_S : (n : Nat) -> (n = plus n Z) -> (S n = S (plus n Z))
283+ plusredZ_S k ih = %runElab (do intro `{{k}}
285+ rewriteWith (Var `{{ih}})
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
294+.. code-block:: idris
296+ Idris> :load elabInteractiveEx4.idr
297+ Type checking ./elabInteractiveEx4.idr
298+ elabInteractiveEx4.idr:7:19-10:43:
300+ 7 | plusredZ_S k ih = %runElab (do intro `{{k}}
301+ | ~~~~~~~~~~~~~~~~~~~~~~~~~ ...
302+ When checking right hand side of plusredZ_S with expected type
305+ Can't use lambda here: type is S k = S (plus k 0)
307+ Holes: Main.plusredZ_S
309+Issues like this are discussed here [#f1]_
311+.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556
245.. |image| image:: ../image/plusReducesProof.png
313.. |image| image:: ../image/plusReducesProof.png