Skip to content

Commit

Permalink
r355
Browse files Browse the repository at this point in the history
  • Loading branch information
@liyishuai
liyishuai committed Jan 5, 2020
1 parent 0f6c9a5 commit c8163f8
Show file tree
Hide file tree
Showing 201 changed files with 201 additions and 201 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;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:36&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:25 UTC 2019 *)
(* Sun Jan 5 03:17:36 UTC 2020 *)
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 Oct 28 08:14:44 UTC 2019 *)
(* Sun Jan 5 03:17:56 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/Basics.html
View file
Original file line number Diff line number Diff line change
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;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:33&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Basics.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1198,4 +1198,4 @@ Fixpoint bin_to_nat (m:bin) : nat
Definition manual_grade_for_binary : option (nat*string) := None.
(** [] *)

(* Mon Oct 28 08:14:23 UTC 2019 *)
(* Sun Jan 5 03:17:33 UTC 2020 *)
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 Oct 28 08:14:26 UTC 2019 *)
(* Sun Jan 5 03:17:37 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/Bib.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">参考文献</span></h1>
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:36&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Bib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,4 +32,4 @@
*)

(* Mon Oct 28 08:14:25 UTC 2019 *)
(* Sun Jan 5 03:17:36 UTC 2020 *)
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 Oct 28 08:14:44 UTC 2019 *)
(* Sun Jan 5 03:17:57 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:25 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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 Oct 28 08:14:42 UTC 2019 *)
(* Sun Jan 5 03:17:55 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:25 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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 Oct 28 08:14:41 UTC 2019 *)
(* Sun Jan 5 03:17:54 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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 Oct 28 08:14:40 UTC 2019 *)
(* Sun Jan 5 03:17:53 UTC 2020 *)
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 Oct 28 08:14:39 UTC 2019 *)
(* Sun Jan 5 03:17:51 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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 Oct 28 08:14:35 UTC 2019 *)
(* Sun Jan 5 03:17:48 UTC 2020 *)
6 changes: 3 additions & 3 deletions lf-current/IndProp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1610,8 +1610,8 @@ <h1 class="libtitle">IndProp<span class="subtitle">归纳定义的命题</span><
<div class="doc">
现在，尽管我们得到了七个分类（正由我们从 <span class="inlinecode"><span class="id" type="var">exp_match</span></span> 的定义中期待的那样），
但 <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> 还是丢失了一个非常重要的信息：<span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 事实上匹配了某种形式的 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>。
这意味着对于<b>全部</b>的七个构造子分类我们都需要给出证明，尽管其中两个（<span class="inlinecode"><span class="id" type="var">MStar0</span></span>
和 <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>）是自相矛盾的。
这意味着对于<b>全部</b>的七个构造子分类我们都需要给出证明，尽管除了其中两个（<span class="inlinecode"><span class="id" type="var">MStar0</span></span>
和 <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>）之外，剩下的五个构造子分类是和前提矛盾的。
我们仍然可以在一些构造子上继续证明，比如 <span class="inlinecode"><span class="id" type="var">MEmpty</span></span>……
</div>
<div class="code code-tight">
Expand Down 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;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

Expand Down
6 changes: 3 additions & 3 deletions lf-current/IndProp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1029,8 +1029,8 @@ Proof.

(** 现在，尽管我们得到了七个分类（正由我们从 [exp_match] 的定义中期待的那样），
但 [H1] 还是丢失了一个非常重要的信息：[s1] 事实上匹配了某种形式的 [Star re]。
这意味着对于_'全部'_的七个构造子分类我们都需要给出证明，尽管其中两个（[MStar0]
和 [MStarApp]）是自相矛盾的。
这意味着对于_'全部'_的七个构造子分类我们都需要给出证明，尽管除了其中两个（[MStar0]
和 [MStarApp]）之外，剩下的五个构造子分类是和前提矛盾的。
我们仍然可以在一些构造子上继续证明，比如 [MEmpty]…… *)

- (* MEmpty *)
Expand Down Expand Up @@ -1831,4 +1831,4 @@ Proof.
(* 请在此处解答 *) Admitted.
(** [] *)

(* Mon Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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 Oct 28 08:14:33 UTC 2019 *)
(* Sun Jan 5 03:17:45 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:33&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:23 UTC 2019 *)
(* Sun Jan 5 03:17:33 UTC 2020 *)
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 Oct 28 08:14:27 UTC 2019 *)
(* Sun Jan 5 03:17:38 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/LICENSE
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Copyright (c) 2019
Copyright (c) 2020

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
Expand Down
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;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:34&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:23 UTC 2019 *)
(* Sun Jan 5 03:17:34 UTC 2020 *)
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 Oct 28 08:14:28 UTC 2019 *)
(* Sun Jan 5 03:17:39 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:34&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:23 UTC 2019 *)
(* Sun Jan 5 03:17:34 UTC 2020 *)
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 Oct 28 08:14:31 UTC 2019 *)
(* Sun Jan 5 03:17:43 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/Maps.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -526,7 +526,7 @@ <h1 class="libtitle">Maps<span class="subtitle">全映射与偏映射</span></h1
</div>

<br/>
<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Maps.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -342,4 +342,4 @@ Proof.
apply t_update_permute.
Qed.

(* Mon Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
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 Oct 28 08:14:34 UTC 2019 *)
(* Sun Jan 5 03:17:46 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:34&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:23 UTC 2019 *)
(* Sun Jan 5 03:17:34 UTC 2020 *)
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 Oct 28 08:14:29 UTC 2019 *)
(* Sun Jan 5 03:17:40 UTC 2020 *)
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;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:36&nbsp;UTC&nbsp;2020&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 Oct 28 08:14:25 UTC 2019 *)
(* Sun Jan 5 03:17:36 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/PostscriptTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Oct 28 08:14:44 UTC 2019 *)
(* Sun Jan 5 03:17:57 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/Preface.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ <h1 class="libtitle">Preface<span class="subtitle">前言</span></h1>
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:22&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:33&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Preface.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,4 +307,4 @@
（National Science Foundation）在 NSF 科研赞助 1521523 号
_'深度规范科学'_ 下提供支持。 *)

(* Mon Oct 28 08:14:22 UTC 2019 *)
(* Sun Jan 5 03:17:33 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/PrefaceTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Oct 28 08:14:25 UTC 2019 *)
(* Sun Jan 5 03:17:36 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/ProofObjects.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -819,7 +819,7 @@ <h1 class="libtitle">ProofObjects<span class="subtitle">柯里-霍华德对应</
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/ProofObjects.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -531,4 +531,4 @@ End MyEquality.
略会将这个事实加入到上下文中。 *)


(* Mon Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/ProofObjectsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,4 +85,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Mon Oct 28 08:14:35 UTC 2019 *)
(* Sun Jan 5 03:17:47 UTC 2020 *)
2 changes: 1 addition & 1 deletion lf-current/Rel.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -587,7 +587,7 @@ <h1 class="libtitle">Rel<span class="subtitle">关系的性质</span></h1>
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Sun&nbsp;Jan&nbsp;5&nbsp;03:17:35&nbsp;UTC&nbsp;2020&nbsp;*)</span><br/>
</div>
</div>

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

(* Mon Oct 28 08:14:24 UTC 2019 *)
(* Sun Jan 5 03:17:35 UTC 2020 *)
Loading

0 comments on commit c8163f8

Please sign in to comment.