我可以在"coqtop-nois"下定义一种策略吗? [英] 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.

我正在重新开发"coqtop -nois"下的"Coq.Init.Prelude"和"HoTT.Basics.Overture".我发现直接编写表达式很困难.这就是为什么我要使用战术.我想知道为什么我不能使用"Ltac".

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

推荐答案

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

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

Declare ML Module "ltac_plugin".

这篇关于我可以在"coqtop-nois"下定义一种策略吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！