Я прохожу курс «Основы логики» и сталкиваюсь со следующими ошибками:
Строки не определены
Lists.v, код:
Definition manual_grade_for_rev_injective : option (nat*string) := None.
Ответ:
Ошибка: строка ссылки не найдена в текущей среде.
После добавления Require Import String. в начало файла ошибка исчезает.Но зачем мне это делать?Я думал, что курс должен работать как есть.
Ошибка предупреждений
Код:
Set Warnings "-notation-overridden,-parsing".
Ответ:
Ошибка: естьПредупреждения отсутствуют.
Я не могу это исправить.
Пустой список "[]" Символ неопределенная ошибка
В файле Logic.v
Lemma in_not_nil :
forall A (x : A) (l : list A), In x l -> l <> [].
Ошибка для []:
Синтаксическая ошибка: ожидается [constr: operconstr] после '<>' (в [constr: operconstr]).
Я не мог это исправить.
Что не так?Пожалуйста, помогите.