idris-proof-script-mode接受哪种语言？

Question

在Emacs中，使用idris-mode 20200522.808，当我使用C-c C-l加载文件时，系统会显示一个孔列表，并显示消息"Press the P button to solve the holes In the prover interactively“。

证明器由两个窗口组成：*idris-proof-obligations*和*idris-proof-script*。但我不明白这是怎么回事。我尝试输入在命令行验证程序中使用的相同术语，如intro `{{x}}和rewriteWith mylemma，但当我键入M-n以"advance“时，我得到了以下错误消息：

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

我应该做些什么呢？

Answer 1

它接受the old theorem prover语言中的证明策略，该语言已被弃用。