我不明白为什么 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.