3 
$ coqtop -nois
Welcome to Coq 8.7.0 (October 2017)

Coq < Ltac i := idtac.
Toplevel input, characters 0-4:
> Ltac i := idtac.
> ^^^^
Error: Syntax error: illegal begin of vernac.

我正在“coqtop -nois”下重新开发“Coq.Init.Prelude”和“HoTT.Basics.Overture”以进行练习。我发现很难直接写表达式。这就是我想使用战术的原因。我想知道为什么我不能使用“Ltac”。

4

1 回答 1

5

Ltac 现在作为插件提供，您需要加载它才能使用：

Declare ML Module "ltac_plugin".
于 2018-02-17T04:46:59.470 回答