Начинающий не может импортировать в Lean

Question

Я абсолютный новичок, а не программист, пытаюсь научиться формальной проверке с помощью Logic and Proof .Я ничего не могу импортировать в Lean.

Я извлекаю 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.Обратите внимание, что, поскольку я новичок, я никогда ничего не компилировал из исходного кода.

Answer 1

Я получил решение, связавшись напрямую с профессором Авигадом.

Оказывается, в книге используется не только стандартная библиотека, но и библиотека математических компонентов Lean, mathlib .Установка у меня сработала.Теперь я могу сделать import data.set без ошибки.

Answer 2

Эти пакеты скрыты в init.

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

Но я считаю, что Lean по умолчанию импортирует все в init, поэтому на самом деле вам не понадобятся строки выше.

Вы также можете пропустить open и квалифицировать вызовы.

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