@@ -270,7 +270,7 @@ because this gives the following error:
270270 unexpected "in"
271271 expecting dependent type signature
272272
273−We can try putting the proof into a seperate function like this:
273+However if we put the proof into a seperate function like this:
274274
275275.. code-block:: idris
276276
@@ -279,34 +279,17 @@ We can try putting the proof into a seperate function like this:
279279
280280 %language ElabReflection
281281
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)
282+ plusredZ_S : (k : Nat) -> (ih:(k = plus k Z)) -> (S k = S (plus k Z))
283+ plusredZ_S = %runElab (do intro `{{k}}
284+ intro `{{ih}}
285+ rewriteWith (Var `{{ih}})
286+ reflexivity)
287287
288288 plusReducesZ' : (n:Nat) -> n = plus n Z
289289 plusReducesZ' Z = %runElab (do reflexivity)
290290 plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih
291291
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]_
292+This then loads.
310293
311294.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556
312295