Начинающий не может импортировать в Lean
Я абсолютный новичок, а не программист, пытающийся научиться формальной проверке с помощью Logic и 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. Обратите внимание, что, поскольку я новичок, я никогда не собирал ничего из исходного кода.
2 ответа
Я получил решение, связавшись напрямую с профессором Авигад.
Оказывается, в книге используется не только стандартная библиотека, но и библиотека математических компонентов Lean, mathlib. Установка у меня сработала. Теперь я могу сделать import data.set без получения ошибки.
Эти пакеты спрятаны в init,
import init.classical
import init.data.nat
import init.data.set
Но я верю, что Лин импортирует все в init по умолчанию, так что на самом деле вам не нужны строки выше.
Вы также можете пропустить open и квалифицировать призывы.
example (P : Prop) : P ∨ ¬ P := classical.em P