Skip to content

Commit

Permalink
r300
Browse files Browse the repository at this point in the history
  • Loading branch information
@liyishuai
liyishuai committed Jul 19, 2019
1 parent 1886c9a commit a29b670
Show file tree
Hide file tree
Showing 199 changed files with 427 additions and 427 deletions.
2 changes: 1 addition & 1 deletion lf-current/Auto.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -799,7 +799,7 @@ <h1 class="libtitle">Auto<span class="subtitle">更多的自动化</span></h1>
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Auto.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -603,4 +603,4 @@ Proof. eauto. Qed.
[e] 开头的变体。 *)


(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/AutoTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:45 UTC 2019 *)
(* Fri Jul 19 00:32:40 UTC 2019 *)
4 changes: 2 additions & 2 deletions lf-current/Basics.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -504,7 +504,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Coq 函数式编程</span></h1
<div class="doc">
这里的模式 <span class="inlinecode"><span class="id" type="var">primary</span></span> <span class="inlinecode"><span class="id" type="var">_</span></span> 是“<span class="inlinecode"><span class="id" type="var">primary</span></span> 应用到除 <span class="inlinecode"><span class="id" type="tactic">red</span></span> 之外的任何 <span class="inlinecode"><span class="id" type="var">rgb</span></span> 构造子”
的简写形式（通配模式 <span class="inlinecode"><span class="id" type="var">_</span></span> 的效果与 <span class="inlinecode"><span class="id" type="var">monochrome</span></span> 定义中的哑（dummy）模式变量
<span class="inlinecode"><span class="id" type="var">p</span></span> 相同。）
<span class="inlinecode"><span class="id" type="var">q</span></span> 相同。）
</div>

<div class="doc">
Expand Down Expand Up @@ -1673,7 +1673,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Coq 函数式编程</span></h1
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
4 changes: 2 additions & 2 deletions lf-current/Basics.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -334,7 +334,7 @@ Definition isred (c : color) : bool :=

(** 这里的模式 [primary _] 是“[primary] 应用到除 [red] 之外的任何 [rgb] 构造子”
的简写形式（通配模式 [_] 的效果与 [monochrome] 定义中的哑（dummy）模式变量
[p] 相同。） *)
[q] 相同。） *)

(* ================================================================= *)
(** ** Tuples *)
Expand Down Expand Up @@ -1198,4 +1198,4 @@ Fixpoint bin_to_nat (m:bin) : nat
Definition manual_grade_for_binary : option (nat*string) := None.
(** [] *)

(* Mon Jul 8 10:06:19 UTC 2019 *)
(* Fri Jul 19 00:32:19 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/BasicsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -192,4 +192,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:22 UTC 2019 *)
(* Fri Jul 19 00:32:22 UTC 2019 *)
10 changes: 5 additions & 5 deletions lf-current/Bib.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,12 +46,12 @@ <h1 class="libtitle">Bib<span class="subtitle">参考文献</span></h1>
<a target="Bertot 2004"><span class="inlineref"><b>[Bertot 2004]</b></span></a> Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and
Pierre Casteran. Springer-Verlag, 2004.
<a href="http://tinyurl.com/z3o7nqu"><span class="inlineref">http://tinyurl.com/z3o7nqu</span></a>
<a href="https://tinyurl.com/z3o7nqu"><span class="inlineref">https://tinyurl.com/z3o7nqu</span></a>

<div class="paragraph"> </div>

<a target="Chlipala 2013"><span class="inlineref"><b>[Chlipala 2013]</b></span></a> Certified Programming with Dependent Types, by
Adam Chlipala. MIT Press. 2013. <a href="http://tinyurl.com/zqdnyg2"><span class="inlineref">http://tinyurl.com/zqdnyg2</span></a>
Adam Chlipala. MIT Press. 2013. <a href="https://tinyurl.com/zqdnyg2"><span class="inlineref">https://tinyurl.com/zqdnyg2</span></a>

<div class="paragraph"> </div>

Expand All @@ -70,21 +70,21 @@ <h1 class="libtitle">Bib<span class="subtitle">参考文献</span></h1>
<a target="Pugh 1991"><span class="inlineref"><b>[Pugh 1991]</b></span></a> Pugh, William. "The Omega test: a fast and practical
integer programming algorithm for dependence analysis." Proceedings
of the 1991 ACM/IEEE conference on Supercomputing. ACM, 1991.
<a href="http://dl.acm.org/citation.cfm?id=125848"><span class="inlineref">http://dl.acm.org/citation.cfm?id=125848</span></a>
<a href="https://dl.acm.org/citation.cfm?id=125848"><span class="inlineref">https://dl.acm.org/citation.cfm?id=125848</span></a>

<div class="paragraph"> </div>

<a target="Wadler 2015"><span class="inlineref"><b>[Wadler 2015]</b></span></a> Philip Wadler. "Propositions as types."
Communications of the ACM 58, no. 12 (2015): 75-84.
<a href="http://dl.acm.org/citation.cfm?id=2699407"><span class="inlineref">http://dl.acm.org/citation.cfm?id=2699407</span></a>
<a href="https://dl.acm.org/citation.cfm?id=2699407"><span class="inlineref">https://dl.acm.org/citation.cfm?id=2699407</span></a>

<div class="paragraph"> </div>


</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
10 changes: 5 additions & 5 deletions lf-current/Bib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@
[Bertot 2004] Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and
Pierre Casteran. Springer-Verlag, 2004.
http://tinyurl.com/z3o7nqu
https://tinyurl.com/z3o7nqu
[Chlipala 2013] Certified Programming with Dependent Types, by
Adam Chlipala. MIT Press. 2013. http://tinyurl.com/zqdnyg2
Adam Chlipala. MIT Press. 2013. https://tinyurl.com/zqdnyg2
[Lipovaca 2011] Learn You a Haskell for Great Good! A Beginner's
Guide, by Miran Lipovaca, No Starch Press, April 2011.
Expand All @@ -24,12 +24,12 @@
[Pugh 1991] Pugh, William. "The Omega test: a fast and practical
integer programming algorithm for dependence analysis." Proceedings
of the 1991 ACM/IEEE conference on Supercomputing. ACM, 1991.
http://dl.acm.org/citation.cfm?id=125848
https://dl.acm.org/citation.cfm?id=125848
[Wadler 2015] Philip Wadler. "Propositions as types."
Communications of the ACM 58, no. 12 (2015): 75-84.
http://dl.acm.org/citation.cfm?id=2699407
https://dl.acm.org/citation.cfm?id=2699407
*)

(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/BibTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:45 UTC 2019 *)
(* Fri Jul 19 00:32:40 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Extraction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,7 @@ <h1 class="libtitle">Extraction<span class="subtitle">从 Coq 中提取 ML</span
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Extraction.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,4 +116,4 @@ Extraction "imp.ml" empty_st ceval_step parse.
(** 有关提取的更多详情见_'软件基础'_第三卷_'已验证的函数式算法'_中的
Extract 一章。 *)

(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ExtractionTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:43 UTC 2019 *)
(* Fri Jul 19 00:32:38 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Imp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2550,7 +2550,7 @@ <h1 class="libtitle">Imp<span class="subtitle">简单的指令式程序</span></
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Imp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1718,4 +1718,4 @@ End BreakImp.
[] *)


(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFun.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,7 @@ <h1 class="libtitle">ImpCEvalFun<span class="subtitle">Imp 的求值函数</span
</div>

<br/>
<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFun.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -369,4 +369,4 @@ Proof.
rewrite E1 in E2. inversion E2. reflexivity.
omega. omega. Qed.

(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFunTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,4 +85,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:42 UTC 2019 *)
(* Fri Jul 19 00:32:37 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ImpParser.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ <h1 class="libtitle">ImpParser<span class="subtitle">用 Coq 实现词法分析
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> "z")%<span class="id" type="var">imp</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">cbv</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/ImpParser.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -454,4 +454,4 @@ Example eg2 : parse "
"x" ::= "z")%imp.
Proof. cbv. reflexivity. Qed.

(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ImpParserTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:41 UTC 2019 *)
(* Fri Jul 19 00:32:36 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ImpTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,4 +246,4 @@ idtac "---------- BreakImp.while_stops_on_break ---------".
Print Assumptions BreakImp.while_stops_on_break.
Abort.

(* Mon Jul 8 10:06:39 UTC 2019 *)
(* Fri Jul 19 00:32:35 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/IndPrinciples.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1014,7 +1014,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">归纳法则</span></h1
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/IndPrinciples.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -591,4 +591,4 @@ Check le_ind.
因此，根据 [le_S]，[n <= S o']。 [] *)

(* Mon Jul 8 10:06:20 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/IndPrinciplesTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:35 UTC 2019 *)
(* Fri Jul 19 00:32:32 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/IndProp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2789,7 +2789,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">归纳定义的命题</span><
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/IndProp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1831,4 +1831,4 @@ Proof.
(* 请在此处解答 *) Admitted.
(** [] *)

(* Mon Jul 8 10:06:20 UTC 2019 *)
(* Fri Jul 19 00:32:20 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/IndPropTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -292,4 +292,4 @@ idtac "---------- filter_challenge ---------".
idtac "MANUAL".
Abort.

(* Mon Jul 8 10:06:32 UTC 2019 *)
(* Fri Jul 19 00:32:30 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Induction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -884,7 +884,7 @@ <h1 class="libtitle">Induction<span class="subtitle">归纳证明</span></h1>
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Induction.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -587,4 +587,4 @@ Definition manual_grade_for_binary_inverse_b : option (nat*string) := None.
Definition manual_grade_for_binary_inverse_c : option (nat*string) := None.
(** [] *)

(* Mon Jul 8 10:06:19 UTC 2019 *)
(* Fri Jul 19 00:32:19 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/InductionTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,4 +177,4 @@ idtac "---------- binary_inverse_c ---------".
idtac "MANUAL".
Abort.

(* Mon Jul 8 10:06:24 UTC 2019 *)
(* Fri Jul 19 00:32:23 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Lists.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1480,7 +1480,7 @@ <h1 class="libtitle">Lists<span class="subtitle">使用结构化的数据</span>
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Lists.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1018,4 +1018,4 @@ Inductive baz : Type :=
Definition manual_grade_for_baz_num_elts : option (nat*string) := None.
(** [] *)

(* Mon Jul 8 10:06:19 UTC 2019 *)
(* Fri Jul 19 00:32:19 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/ListsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -473,4 +473,4 @@ idtac "---------- rev_injective ---------".
idtac "MANUAL".
Abort.

(* Mon Jul 8 10:06:25 UTC 2019 *)
(* Fri Jul 19 00:32:24 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Logic.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1948,7 +1948,7 @@ <h1 class="libtitle">Logic<span class="subtitle">Coq 中的逻辑系统</span></
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Logic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1389,4 +1389,4 @@ Definition implies_to_or := forall P Q:Prop,

[] *)

(* Mon Jul 8 10:06:19 UTC 2019 *)
(* Fri Jul 19 00:32:20 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/LogicTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -390,4 +390,4 @@ idtac "---------- not_exists_dist ---------".
Print Assumptions not_exists_dist.
Abort.

(* Mon Jul 8 10:06:29 UTC 2019 *)
(* Fri Jul 19 00:32:27 UTC 2019 *)
4 changes: 2 additions & 2 deletions lf-current/Maps.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ <h1 class="libtitle">Maps<span class="subtitle">全映射与偏映射</span></h1

<div class="doc">
标准库的文档见
<a href="http://coq.inria.fr/library/">http://coq.inria.fr/library/</a>。
<a href="https://coq.inria.fr/library/">https://coq.inria.fr/library/</a>。

<div class="paragraph"> </div>

Expand Down Expand Up @@ -526,7 +526,7 @@ <h1 class="libtitle">Maps<span class="subtitle">全映射与偏映射</span></h1
</div>

<br/>
<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
4 changes: 2 additions & 2 deletions lf-current/Maps.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ From Coq Require Import Lists.List.
Import ListNotations.

(** 标准库的文档见
http://coq.inria.fr/library/。
https://coq.inria.fr/library/。

[Search] 指令可用于查找涉及具体类型对象的定理。我们花点时间来熟悉一下它。 *)

Expand Down Expand Up @@ -342,4 +342,4 @@ Proof.
apply t_update_permute.
Qed.

(* Mon Jul 8 10:06:20 UTC 2019 *)
(* Fri Jul 19 00:32:20 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/MapsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,4 +75,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Jul 8 10:06:33 UTC 2019 *)
(* Fri Jul 19 00:32:30 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Poly.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1541,7 +1541,7 @@ <h1 class="libtitle">Poly<span class="subtitle">多态与高阶函数</span></h1

<span class="id" type="keyword">End</span> <span class="id" type="var">Church</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Exercises</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:19&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:20&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Poly.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1060,4 +1060,4 @@ End Church.
End Exercises.


(* Mon Jul 8 10:06:19 UTC 2019 *)
(* Fri Jul 19 00:32:20 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/PolyTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -421,4 +421,4 @@ idtac "---------- Exercises.Church.exp_3 ---------".
Print Assumptions Exercises.Church.exp_3.
Abort.

(* Mon Jul 8 10:06:26 UTC 2019 *)
(* Fri Jul 19 00:32:25 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Postscript.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Jul&nbsp;8&nbsp;10:06:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Jul&nbsp;19&nbsp;00:32:21&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Postscript.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,4 +81,4 @@
https://deepspec.org/event/dsss17/index.html
*)

(* Mon Jul 8 10:06:21 UTC 2019 *)
(* Fri Jul 19 00:32:21 UTC 2019 *)
Loading

0 comments on commit a29b670

Please sign in to comment.