Я только начинаю изучать coq, и я в основном скопировал код (?) Из того, что профессор показал в классе, но он никогда не работал на моем ноутбуке!
Я понятия не имею, почему он продолжает говорить мне, что ссылка y не была найдена в текущей среде.
И в моем кокаиде только два предложения (?):
Require Export Utf8.
Notation "x->y" :=(x->y)(at level 99).
Я читал некоторые веб-страницы с похожими вопросами, но я не думаю, что у нас была такая же проблема. Если я не прав, извините за это.
Кроме того, не могли бы вы сказать, что означают слова "Utf8" и "на уровне 99" ??
Я знаю, что это глупые вопросы, но я просто не понимаю.
Спасибо, что взглянули на это:)