如何像在 CoqIde/jscoq 中一样激活 vscode/vscoq 中的 Coq 消息？
我期待消息栏中出现一些内容，但没有看到它
示例脚本：
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.
在 JScoq 中我看到 (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)
在 vscode 中我什么也没看到。
查看图片以确保清晰度 
交叉：
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:
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
似乎打印在：
Seems it's printed in: