如何解决在 Emacs 证明通用目标缓冲区中丢失了“.+1”Coq 符号
我想在运行 Catalina 的 Mac 上升级 Emacs(目前为 26.1,来自 emacsformacosx.com,直接从 High Sierra 导入,使用 PG 4.5-git),并发现 Apple 在此版本的 Mac 上让 Emacs 变得困难操作系统引入了“检查恶意软件”,这似乎很难绕过。
我恢复到我以前的 Emacs 版本,但是,从那时起,SSReflect .+1
的 nat
表示法无法在 PG 的 Coq 目标缓冲区中正确显示(我自己的表示法得到了正确管理,尽管)。它显示为标准的 succn
构造函数。
有谁知道可能是什么问题(FWIW,我正在使用 CoQ 的 NixOS 版本)?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。