19:04:53	 From Jiajie Chen : 学习
19:05:00	 From Jiajie Chen : 是哪个插件
19:05:06	 From dram : vscoq
19:06:46	 From Jiajie Chen : yes
19:06:48	 From ZhiSheng Yuan : 可以（
19:14:48	 From Jiajie Chen : 看不懂法语
19:15:02	 From Ocean Shen : lean！
19:15:32	 From dram : 按照你用中文能力看日文的方式用你英文能力看法文就好了
19:19:03	 From 李拯先 : 越来读cok呀，我以为读co q的
19:19:44	 From dram : 法语，法语……
19:21:04	 From Xh : > The name coq means "rooster" in French and stems from a French tradition of naming research development tools after animals.
19:21:47	 From Ocean Shen : 自举还行
19:23:03	 From Pengcheng Xu : 有沒有用 Coq 做算法題的
19:23:22	 From Ocean Shen : codewars 上有 coq 题目（
19:23:37	 From 李拯先 : software foundations 第三册好像涉及到
19:24:00	 From dram : 等会儿就讲到了嘛，别着急
19:25:59	 From 李拯先 : AWS是不是搞过形式化验证
19:27:28	 From dram : TLA+ 和 Coq 的这个做的事情不完全一样
20:11:53	 From Pengcheng Xu : https://stackoverflow.com/questions/14917318/verbose-auto-in-coq
20:13:42	 From dram : Set Info Auto.
22:04:30	 From Ocean Shen : emacs 当 ide 挺好的（
22:04:40	 From dram : 没有 intellij 好
22:17:54	 From Ocean Shen : intellj 可以 coq 吗（
22:18:19	 From Pengcheng Xu : https://github.com/enriquerodbe/coqidea
22:18:45	 From Pengcheng Xu : https://github.com/editor-plugins/intellij-coq
22:18:53	 From Pengcheng Xu : 都是 16 年之前的
22:19:17	 From Pengcheng Xu : 2016
22:19:26	 From Pengcheng Xu : 不是 sixteen years ago
22:20:01	 From Ocean Shen : 都不能把 forall 格式化成反A的那个符号（
22:20:04	 From Pengcheng Xu : https://plugins.jetbrains.com/plugin/10209-lsp-support
22:20:54	 From Pengcheng Xu : https://microsoft.github.io/language-server-protocol/
22:25:31	 From Ocean Shen : Isabelle 就会 import 的时候查一遍
22:25:54	 From Ocean Shen : 打个 import ZFC 然后等十分钟才能开始写（