Coq - VSCode 以蓝色突出显示计算命令

Question

我不明白为什么 Visual Studio Code 用蓝色下划线计算命令。错误消息没有说明这一点。

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.

Answer 1

没有错误信息。错误用红色下划线表示，警告用橙色下划线表示。

蓝色表示有一条与该命令相关的消息，但这不是一条坏消息，只是命令的输出。

如果将指针放在蓝线上，它将显示

Compute

命令的输出。