我不明白为什么 Visual Studio Code 用蓝色下划线标记 Compute 命令。错误消息没有说明这一点。
Inductive day : Type :=
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Compute (next_weekday friday).
Compute (next_weekday (next_weekday saturday)).
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
没有错误消息。错误以红色下划线表示，警告以橙色下划线表示。
蓝色表示有与命令相关的消息，但这不是坏消息，只是命令的输出。
如果将指针放在蓝线上，它将显示
Compute命令的输出。