'How to activate the Coq messages in vscode/vscoq like in the CoqIde/jscoq?
I am expecting something in my messages bar but I don't see it
Example script:
Fixpoint add_left (n m : nat) : nat :=
match n with
| O => m
| S p => S (add_left p m)
end.
Lemma demo_1 :
forall (n : nat),
add_left n O = n.
Proof.
intros. (* goal : add_left n O = n *)
let add_left_red := eval red in add_left in (* reduce add_left, but leave goal alone *)
idtac add_left_red. (* print the result *)
(* Print eval. gives error *)
Print red.
Print add_left_red.
admit.
Abort.
in JScoq I see (https://coq.vercel.app/scratchpad.html):
(fix add_left (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add_left p m)
end)
in vscode I see nothing.
See pics for clarity
cross:
Solution 1:[1]
Seems it's printed in:
It's not a bug, it's not printed in "Notices" but in "Info".
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|---|
| Solution 1 | Charlie Parker |