Yishuai Li
It'll be nice to fold long definitions into: ```coq Definition foo := match bar with | Bar1 => [...] | Bar2 => [...] end. ``` so that they can fit...
Currently both Reset and Save are grey. Consider changing Save to green and Reset to Red?
Fixes #120 ## 相关讨论 - https://github.com/sparanoid/chinese-copywriting-guidelines/issues/114#issuecomment-609048944 ## 待办事项 - [ ] 将英文书刊名的标示方法列入本指南； - [ ] 根据当地标准，更新繁体中文版。
引述现行标准
尊敬的开发者、维护人员： 你们好！ 在下国语不精，谨以普通话、简体字陈述。 了解本项目之前，我排版主要依据如下标准： - 中华人民共和国国家标准GB/T 15834—2011号《标点符号用法》 - 中华人民共和国新闻出版行业标准CY/T 154—2017号《中文出版物夹用英文的编辑规范》 其中部分规则与此处略有出入，例如： - > 中英文之间需要增加空格 异于《中文出版物夹用英文的编辑规范》第8.1节： > 中文文本中夹用英文时，应根据所选用的中英文字体、字符间距以及排版的视觉效果决定英文词句与中文文字之间是否留有空格间距。如留空格，应保证体例的统一。 - > 不重复使用标点符号 #32 已讨论。 - > 简体中文使用直角引号 #83 称其不合规，但根据《标点符号用法》第5.2节“竖排文稿标点符号的位置和书写形式”： > 5.2.3 引号改用双引号“﹃”“﹄”和单引号“﹁”“﹂”，……...
#### Description of the problem As mentioned in QuickChick/QuickChick#294, QuickChick extracts Z to either integer or big integer based on the underlying Coq version, because the ideal extraction module only...
Hope: ```coq Check [1; 2; 3]. ``` where elements are left-aligned. Observed: ```coq Check [1; 2; 3]. Check [ 1; 2; 3]. Check [1 ;2 ;3]. ```
Currently we have: ```coq 1,2: foo; bar. ``` with `coq-indent-semicolon-tactical` spaces in front of `bar` (this example shows the default 2). We should indent `bar` from `foo`, rather than `1,2`.
https://github.com/QuickChick/QuickChick/blob/bbf107056c6623862db843c93e6093a9abe3ad07/test/plugin/plugin.v#L14-L17 > The command has indeed failed with message: Anomaly "Uncaught exception Failure("Internal QuickChick Error : Arguments to result of constructor goodBaz can only be variables or constructors applied to...
Say that we have mutually inductive data types: ``` Inductive A := a | fromB : B -> A with B := b | fromA : A -> B. ```...
Given an inductive data type: ``` Inductive A := a : A | b : A * A -> A. ``` `Derive Show for A.` fails with: > Error: Unable...