警告：“改为从 IDE 菜单设置此选项”在coq中
我正在学习软件基础的“Imp”一章。我在 Coq Ide 中运行了命令Unset Printing Coercions.，coq 消息警告我“改为从 IDE 菜单设置此选项”，显然该命令不起作用。我想也许这个命令在 Coq 提示符环境下可以工作，但是我想知道如果我想在 Coq Ide 中使用“Unset Printing”命令我应该做什么？
I'm studying the Chapter "Imp" of Software foundation. I runned the command Unset Printing Coercions. in Coq Ide, the coq Message warned me that "Set this option from the IDE menu instead" and obviously the command doesn't work. I guess maybe this command will work in the Coq prompt environment, But I want to know what I should do if I want to use "Unset Printing" command in Coq Ide?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您应该进入“查看”菜单，然后勾选/取消勾选“显示强制”按钮。
You should go under the "View" menu, and tick/untick the "Display coercions" button.