我正在通过逻辑基础课程并面临以下错误：
未定义的字符串
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] 中）。
我无法修复它。
怎么了？请帮忙。