0

我从 github 存储库编译了 Lean 2。然后，按照 scr/emacs/README.md 中的说明，我修改了我的 .emacs 文件，打开一个文件，单击“创建新项目”，单击“打开”，输入“hott”并按 Enter。

然后我输入

print eq.inverse

我收到了一条消息

1:1: print result:

1:17: invalid print command

我也尝试lean-hott-mode了相同结果的命令。

我究竟做错了什么？

4

1 回答 1

1

我已经想通了。

显然，Lean 要求 HoTT 文件具有扩展名 *.hlean

于 2019-09-17T19:18:38.880 回答