1

我是 HOL4 和 Emacs 的新手。为这个可能很愚蠢的问题道歉。

我希望按照https://hol-theorem-prover.org/HOL-interaction.pdf的说明为 HOL4 设置 Emacs 。我试图在 Emacs 上启动 HOL 进程Alt-h h并按下Enter，但 Emacs 返回Symbol’s function definition is void: if-let*。我.emacs.d/init.el的定义如下。我应该怎么做才能修复错误？谢谢。

;; Added by Package.el.  This must come before configurations of
;; installed packages.  Don't delete this line.  If you don't want it,
;; just comment it out by adding a semicolon to the start of the line.
;; You may delete these explanatory comments.
(package-initialize)
(transient-mark-mode 1)
(load "/home/user/HOL/tools/hol-mode")
(load "/home/user/HOL/tools/hol-unicode")
4

1 回答 1

0

错误消息“Symbol's function definition is void: if-let*”表示被调用函数在调用if-let*时不可用（不是“预加载”）。由于您在“尝试启动 HOL 进程”时编写了此代码，因此该函数很可能是由HOL库调用的。

要查找函数定义所在的位置，请键入C-h f <if-let*>(command M-x describe-function) 1。在我的设置中，输出以以下行开头：

if-let* is a Lisp macro in ‘subr-x.el’

这意味着if-let*在文件中定义subr-x.el（它公开了库subr-x）。这个图书馆的评论部分说：

如果你想使用这个库，使用它几乎总是正确的：

(eval-when-compile (需要'subr-x))

因此，将以下行添加到.emacs.d/init.el加载HOL库之前应该可以解决问题：

(eval-when-compile (require 'subr-x))

[虽然通常只使用 . 加载库(require '<library-name>)。]

请注意，函数的确切位置可能取决于 GNU Emacs 版本和/或设置的其他细节。如果手头没有这些信息，这个答案试图解释如何以一般方式解决这个问题。（当提出问题时，建议指定 GNU Emacs 的版本并提供在没有用户配置的情况下调用 Emacs 的复制步骤：emacs -Q。）

  1. Emacs 键符号
于 2021-12-28T16:06:54.547 回答