In Emacs, with idris-mode 20200522.808, when I load the file using C-c C-l, I'm presented with a list of holes, and the message "Press the [P] buttons to solve the holes interactively in the prover."
The prover consists of two windows, *idris-proof-obligations* and *idris-proof-script*. But I can't figure out how this is supposed to work. I tried typing in the same sort of terms I would use in the command-line prover, like intro `{{x}} and rewriteWith mylemma, but when I type M-n to "advance", I got these error messages:
Prover error: (input):1:7:
|
1 | intro ‘{{n}}
| ^
unexpected ’‘’
expecting end of input or name
Prover error: (input):1:8:
|
1 | rewriteWith sym (fibAuxEq 0 1 n)
| ^
unexpected ’W’
expecting tactic
What should I be doing instead?
