問題タブ [lean]

と を考える(a : Z)と、そんな(a >= 0)ことをしたいと思います。もちろん、これは異種の平等であるため、少し面倒です。(n : N)n = an = a

nat_abs負の整数がある場合も処理することを除いて、このようなことを行うものを見つけましたが、それはわかっていません。

リーンでは、この状況にどのように対処しますか?

私はプログラマーではなく、絶対的な初心者であり、Logic と Proofを使用して正式な検証を学ぼうとしています。リーンでは何もインポートできません。

バイナリの tar ファイルを抽出して/tmp実行します。

何かをインポートするとき以外は機能します。だから私のファイルtest.leanがちょうど言うなら

エラーはありません。しかし、同じファイルが代わりに言う場合

エラーメッセージが表示されます

で同様のエラーが発生しimport data.natます。

私は何を間違っていますか? どうすればよいですか? Ubuntu 16.04 を使用しています。私は初心者なので、ソースから何もコンパイルしたことがないことに注意してください。