Search code examples
coqcoq-tacticltac

Can I define a tactic under "coqtop - nois"?

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

I am redeveloping "Coq.Init.Prelude" and "HoTT.Basics.Overture" under "coqtop -nois" for pratice. I find it hard to write expressions directly. That's why I want to use tactics. I wonder why I can not use "Ltac".

Solution

  • Ltac is now provided as a plugin, which you’ll need to load to use:

    Declare ML Module "ltac_plugin".