+ Thursday, Apriil 4, 2019, 20:20:00
OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - environmental parametrized module 1 - 环境的 参数化了 包裹 1
https://www.bilibili.com/video/av48293615/

+ Friday, April 5, 2019, 22:22:00
OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - environmental parametrized module 2 - 环境的 参数化了 包裹 2
https://www.bilibili.com/video/av48424625/

+ Friday, April 5, 2019, 22:44:00
OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - environmental parametrized module 3 - 环境的 参数化了 包裹 3
https://www.bilibili.com/video/av48426398/

Alt+↑/↓ – move through proof; Alt+→ or Alt+⏎ – go to cursor.
Alt+hover executed sentences to watch intermediate steps.
Hover identifiers in goals to view their types. Alt+hover to view definitions.
Company-coq addon is enabled: it will auto-complete names of tactics and lemmas from the standard library, and also show types of lemmas in the right pane.

“Alt +↑/↓” : 通过证明。 “Alt +→”或“Alt +⏎” : 转到光标。
“Alt +”悬停执行句子以观察中间步骤。
将目标中的标识符悬停在其中以查看其类型。 “Alt +”悬停以查看定义。
启用“Company-coq”加载项:它将自动完成标准库中的策略和引理名称,并在右侧窗格中显示引导类型。