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

しかし、リーンはデフォルトですべてをインポートすると信じているinitので、実際には上記の行は必要ありません。

open呼び出しをスキップして修飾することもできます。

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