+ ‎Saturday, ‎March ‎9, ‎2019, ‏‎00:37:41
OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - logic , variables , proof - 逻辑，变量，证明
https://www.bilibili.com/video/av45747037

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”加载项：它将自动完成标准库中的策略和引理名称，并在右侧窗格中显示引导类型。

From Qoc Require Import Jisuanji . 归纳的 我的二进制 := 真 : 我的二进制 | 假 : 我的二进制 . 定义 abc或 ( x : 我的二进制 ) ( y : 我的二进制 ) := ( 若 x 则 真 否则 y ) . (** true or true = true. 1 + 1 = 1 true or false = true. 1 + 0 = 1 false or true = true. 0 + 1 = 1 false or false = false. 0 + 0 = 0 *) 部分 我的分1. 变量 x : 我的二进制. 变量 y : 我的二进制. 论点 我的论点1 : abc或 x y = abc或 y x . 证明. 展开 abc或. 例子 x. - (** x 真*) 例子 y. + (** y 真 *) 同一. + (** y 假 *) 同一. - (** x 假 *) 例子 y. + (** y 真 *) 同一. + (** y 假 *) 同一. 据证实. 结束 我的分1. (** Guīnà yì wǒ de èrjìnzhì := Zhēn: Wǒ de èrjìnzhì | jiǎ: Wǒ de èrjìnzhì. Dìngyì huò (x : Wǒ de èrjìnzhì) (y : Wǒ de èrjìnzhì):= (Ruò x zé zhēn fǒuzé y). Bùfèn wǒ de fēn 1. Biànliàng x: Wǒ de èrjìnzhì. Biànliàng y: Wǒ de èrjìnzhì. Lùndiǎn wǒ dì lùndiǎn 1: Huò x y = huò y x. Zhèngmíng. Zhǎnkāi huò. Lìzi x. - Lìzi y. + Tóngyī. + Tóngyī. - Lìzi y. + Tóngyī. + Tóngyī. Jù zhèngshí. Jiéshù wǒ de fēn 1. *)