2

我是一个绝对的初学者，而不是程序员，正在尝试使用Logic 和 Proof学习形式验证。我不能在精益中导入任何东西。

我提取二进制文件的 tar 文件，/tmp然后执行

/tmp/lean-3.4.1-linux/bin/./lean /tmp/test.lean

除非我导入任何东西，否则它可以工作。所以如果我的文件test.lean只是说

open classical
example (P : Prop) : P ∨ ¬ P := em P

没有错误。但是，如果相同的文件改为说

import data.set

我收到错误消息

/tmp/test.lean:1:0: error: file 'data/set' not found in the LEAN_PATH  
/tmp/test.lean:1:0: error: invalid import: data.set  
could not resolve import: data.set

类似的错误发生在import data.nat.

我做错了什么，我该怎么办？我正在使用 Ubuntu 16.04。请注意，由于我是初学者，我从未从源代码编译过任何东西。

4

2 回答 2

1

我通过直接联系 Avigad 教授得到了解决方案。

事实证明，这本书不仅使用了标准库，还使用了精益数学组件库mathlib。安装它对我有用。我现在可以做import data.set而不会出错。

于 2018-06-26T21:31:46.160 回答
0

这些包隐藏在init.

import init.classical
import init.data.nat
import init.data.set

但我相信 Leaninit默认情况下会导入所有内容，因此您实际上不需要上面的行。

您还可以跳过open和限定调用。

example (P : Prop) : P ∨ ¬ P := classical.em P
于 2018-06-26T20:26:03.140 回答