visual-studio-codecoq

Coq - VSCode highlight Compute command in blue

enter image description here

I don't understand why Visual Studio Code underline Compute command in blue. The error message tell nothing about that.

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.
Solution

  • There is no error message. Errors are underlined in red, and warnings in orange.

    Blue means that there is a message associated with the command, but it's not a bad message, just the output of the command.

    If you put your pointer over the blue line, it will show the output of the Compute command.