Short ：the objective of the "鸡算计.在线" is to enable everyone to read and write mathematics . In the next 5 years to 10 years , this could be used in the national education .

短 : “鸡算计.在线”的目的是让每个人都能读写数学。在未来5年到10年，这可以用于国民教育。

• https://space.bilibili.com/403144043

• qoc_jisuanji_logic_variables_proof
• qoc_jisuanji_inductive
• qoc_jisuanji_polymorphism_notation
• qoc_jisuanji_parameter_option
• qoc_jisuanji_tactics
• qoc_jisuanji_environmental_parametrized_module
• qoc_jisuanji_tactical
• qoc_jisuanji_search_error
• qoc_jisuanji_ends

• 수탉수학

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 . (** 短 : “鸡算计.在线”的目的是让每个人都能读写数学。在未来5年到10年，这可以用于国民教育。 Short ：the objective of the "鸡算计.在线" is to enable everyone to read and write mathematics . In the next 5 years to 10 years , this could be used in the national education . Outline :: * PART 1 : ENDS . 第1部分 : 目的们 * PART 2 : INTRODUCTION . 第2部分： 介绍 *) (** * PART 1 : ENDS . 第1部分 : 目的们 *) (** http://鸡算计.在线 http://xn--lzzm24a52n.xn--3ds443g/ 短 : “鸡算计.在线”的目的是让每个人都能读写数学。在未来5年到10年，这可以用于国民教育。 Short ：the objective of the "鸡算计.在线" is to enable everyone to read and write mathematics . In the next 5 years to 10 years , this could be used in the national education . *) (** * PART 2 : INTRODUCTION . 第2部分： 介绍 *) From Qoc Require Import Jisuanji . (** numbers : 0 ; 1 = 0 +1 ; 2 = 1 +1 ; 3 = 2 +1 ... *) 归纳的 infiniteNumbers := Zero : infiniteNumbers | NextOne : infiniteNumbers -> infiniteNumbers . 校验 (NextOne Zero) . 失败了 校验 (NextOne NextOne) . (** addition : 2 ++ 3 = (2 ++ 2) +1 = ((2 ++ 1) +1) +1 = (((2 ++ 0) +1) +1) +1 = ((2 +1) +1) +1 = 5 *) 定义 addMore : infiniteNumbers -> infiniteNumbers -> infiniteNumbers. 证明. 加细 ( 作用 pOutside => _ ) . 加细 ( 固定 innerAddMore yInside := 匹配 yInside 与 Zero => pOutside | NextOne xInside => _ 结束 ) . 加细 ( NextOne (innerAddMore xInside) ) . 定义了 . 打印 addMore . 设置 打印 全都 . 打印 addMore . 计算 ( addMore Zero (NextOne Zero) ) . Reset infiniteNumbers. (** numbers : 0 ; 1 = 0 +1 ; 2 = 1 +1 ; 3 = 2 +1 ... *) Inductive infiniteNumbers := Zero : infiniteNumbers | NextOne : infiniteNumbers -> infiniteNumbers . Check (NextOne Zero) . Fail Check (NextOne NextOne) . (** addition : 2 ++ 3 = (2 ++ 2) +1 = ((2 ++ 1) +1) +1 = (((2 ++ 0) +1) +1) +1 = ((2 +1) +1) +1 = 5 *) Definition addMore : infiniteNumbers -> infiniteNumbers -> infiniteNumbers. Proof. refine ( fun pOutside => _ ) . refine ( fix innerAddMore yInside := match yInside with Zero => pOutside | NextOne xInside => _ end ) . refine ( NextOne (innerAddMore xInside) ) . Defined . Print addMore . Set Printing All . Print addMore . Compute ( addMore Zero (NextOne Zero) ) . (** [Shanghai picture] Hello all the reviewers! I am KwtKat, somewhere in Shanghai China near the two rivers, and my October 2019 would be boring except for this IMPORTANT NEWS !! [School website] I have enlisted in the @anthroplogic.com school, and I chose the english-chinese translator project, for the computer mathematics COQ. [Inria website] COQ is the computer software to read and write all the mathematics, from the high school student to the university researcher. Download COQ now from this website : coq.inria.fr . [Emacs COQ window] So I am KwtKat , your english-chinese translator, for anything COQ ( fried chicken , omelette ... ). I translate the COQ terms expressions and formulas. I translate the COQ definition commands. I translate the COQ proof tactics. I translate the COQ environment parameter settings. I translate the COQ error messages. [Emacs OCAML window] My translation does not damage the COQ correctness, because it touches only the plug-in surface of COQ. [Youtube website; School website] Download and post your questions , reviews and ideas, from the school Bilibili Youtube videos @OOO1337777 , or from the school website @anthroplogic.com . Bye Bye from KwtKat @OOO1337777 school . *) (* 您好所有的评论者！我是KwtKat， 中国上海某处靠近两条河流的地方， 除了这个重要新闻外，我的2019年10月将很无聊！ 我已经加入@ anthroplogic.com学校， 我选择了英文翻译项目， 用于计算机数学的COQ。 COQ是用于读写所有数学的计算机软件， 从高中生到大学研究员。 立即从以下网站下载COQ：coq.inria.fr。 我是KwtKat，您的英语翻译， 用于任何COQ（炸鸡，煎蛋卷...）。 我翻译了COQ术语表达式和公式。 我翻译了COQ定义命令。 我翻译了COQ证明策略。 我翻译了COQ环境参数设置。 我翻译了COQ错误消息。 我的翻译不会破坏COQ的正确性， 因为它仅接触COQ的插入表面。 下载并发布您的问题，评论和想法， 来自学校Bilibili Youtube视频@ OOO1337777， 或从学校网站@ anthroplogic.com。 来自KwtKat @ OOO1337777学校的再见。 *)