coqide - CoqIDE：在当前环境中找不到引用
问题描述
我刚开始学习coq，我基本上是从教授在课堂上展示的代码中复制了代码（？），但它从来没有在我的笔记本电脑上工作过！我不知道为什么它一直告诉我在当前环境中找不到引用 y。我的 coqIDE 中只有两句话（？）：
Require Export Utf8.
Notation "x->y" :=(x->y)(at level 99).
我读过一些网页询问类似的问题，但我认为我们没有同样的问题。如果我错了，很抱歉。另外，你能告诉我“Utf8”和“99级”是什么意思吗？
我知道这些都是愚蠢的问题，但我就是不明白。感谢您查看它:)