Hello,
if you cut and paste the second Elab proof displayed at the bottom of the Automatic Theorem Proving documentation (http://docs.idris-lang.org/en/latest/proofs/interactive.html), into the second 'hole' in the example code, an error message stating that "in" is "unexpected" is displayed.
Steps to Reproduce
import Pruviloj
import Pruviloj.Induction
%language ElabReflection
plusReducesZ' : (n:Nat) -> n = plus n Z
plusReducesZ' Z = %runElab (do reflexivity)
plusReducesZ' (S k) = let ih = plusReducesZ' k in
%runElab (do intro `{{k}}
intro `{{ih}}
compute
rewriteWith (Var `{{ih}})
reflexivity)
Expected Behavior
The compiler should not generate any errors
(cf. "Again, we can cut & paste this into the hole in the original file." statement at the bottom of the aforementioned documentation page).
Hello, if you cut and paste the second Elab proof displayed at the bottom of the Automatic Theorem Proving documentation (http://docs.idris-lang.org/en/latest/proofs/interactive.html), into the second 'hole' in the example code, an error message stating that "in" is "unexpected" is displayed.
Steps to Reproduce
Expected Behavior
The compiler should not generate any errors (cf. "Again, we can cut & paste this into the hole in the original file." statement at the bottom of the aforementioned documentation page).
Observed Behavior