Могу ли я определить тактику в разделе "coqtop - nois"?

Question

$ 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.

Я перерабатываю "Coq.Init.Prelude" и "HoTT.Basics.Overture" под "coqtop -nois" для практики. Мне трудно писать выражения напрямую. Вот почему я хочу использовать тактику. Интересно, почему я не могу использовать "Ltac".

Answer 1

Ltac теперь предоставляется как плагин, который вам нужно загрузить, чтобы использовать:

Declare ML Module "ltac_plugin".