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?
It accepts proof tactics in the language of the old theorem prover, which is deprecated.