Skip to content

Commit

Permalink
r284
Browse files Browse the repository at this point in the history
  • Loading branch information
@liyishuai
liyishuai committed Mar 15, 2019
1 parent 563b642 commit a58f574
Show file tree
Hide file tree
Showing 195 changed files with 579 additions and 706 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:05&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&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] 开头的变体。 *)


(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 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.

(* Fri Mar 15 15:02:23 UTC 2019 *)
(* Fri Mar 15 16:36:45 UTC 2019 *)
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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:02&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:25&nbsp;UTC&nbsp;2019&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.
(** [] *)

(* Fri Mar 15 15:02:02 UTC 2019 *)
(* Fri Mar 15 16:36:25 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.

(* Fri Mar 15 15:02:06 UTC 2019 *)
(* Fri Mar 15 16:36:28 UTC 2019 *)
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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:05&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&nbsp;UTC&nbsp;2019&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 @@
*)

(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 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.

(* Fri Mar 15 15:02:24 UTC 2019 *)
(* Fri Mar 15 16:36:45 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:05&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&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 一章。 *)

(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 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.

(* Fri Mar 15 15:02:22 UTC 2019 *)
(* Fri Mar 15 16:36:43 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:04&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&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.
[] *)


(* Fri Mar 15 15:02:04 UTC 2019 *)
(* Fri Mar 15 16:36:27 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:05&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&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.

(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 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.

(* Fri Mar 15 15:02:21 UTC 2019 *)
(* Fri Mar 15 16:36:42 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:05&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&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.

(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 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.

(* Fri Mar 15 15:02:20 UTC 2019 *)
(* Fri Mar 15 16:36:41 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.

(* Fri Mar 15 15:02:19 UTC 2019 *)
(* Fri Mar 15 16:36:40 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 @@ -1015,7 +1015,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">归纳法则</span></h1
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:04&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:26&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 @@ -592,4 +592,4 @@ Check le_ind.
因此，根据 [le_S]，[n <= S o']。 [] *)

(* Fri Mar 15 15:02:04 UTC 2019 *)
(* Fri Mar 15 16:36:26 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.

(* Fri Mar 15 15:02:15 UTC 2019 *)
(* Fri Mar 15 16:36:37 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:04&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:26&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.
(** [] *)

(* Fri Mar 15 15:02:04 UTC 2019 *)
(* Fri Mar 15 16:36:26 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.

(* Fri Mar 15 15:02:13 UTC 2019 *)
(* Fri Mar 15 16:36:35 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:02&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:25&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.
(** [] *)

(* Fri Mar 15 15:02:02 UTC 2019 *)
(* Fri Mar 15 16:36:25 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.

(* Fri Mar 15 15:02:07 UTC 2019 *)
(* Fri Mar 15 16:36:29 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:03&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:25&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.
(** [] *)

(* Fri Mar 15 15:02:03 UTC 2019 *)
(* Fri Mar 15 16:36:25 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.

(* Fri Mar 15 15:02:08 UTC 2019 *)
(* Fri Mar 15 16:36:30 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:03&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:26&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,

[] *)

(* Fri Mar 15 15:02:03 UTC 2019 *)
(* Fri Mar 15 16:36:26 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.

(* Fri Mar 15 15:02:11 UTC 2019 *)
(* Fri Mar 15 16:36:33 UTC 2019 *)
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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:04&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:26&nbsp;UTC&nbsp;2019&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 @@ -341,4 +341,4 @@ Proof.
apply t_update_permute.
Qed.

(* Fri Mar 15 15:02:04 UTC 2019 *)
(* Fri Mar 15 16:36:26 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.

(* Fri Mar 15 15:02:14 UTC 2019 *)
(* Fri Mar 15 16:36:36 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:03&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:25&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.


(* Fri Mar 15 15:02:03 UTC 2019 *)
(* Fri Mar 15 16:36:25 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.

(* Fri Mar 15 15:02:08 UTC 2019 *)
(* Fri Mar 15 16:36:31 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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:05&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&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
*)

(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 UTC 2019 *)
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.

(* Fri Mar 15 15:02:24 UTC 2019 *)
(* Fri Mar 15 16:36:45 UTC 2019 *)
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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:02&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:25&nbsp;UTC&nbsp;2019&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 号
_'深度规范科学'_ 下提供支持。 *)

(* Fri Mar 15 15:02:02 UTC 2019 *)
(* Fri Mar 15 16:36:25 UTC 2019 *)
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.

(* Fri Mar 15 15:02:05 UTC 2019 *)
(* Fri Mar 15 16:36:27 UTC 2019 *)
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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:04&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:26&nbsp;UTC&nbsp;2019&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.
略会将这个事实加入到上下文中。 *)


(* Fri Mar 15 15:02:04 UTC 2019 *)
(* Fri Mar 15 16:36:26 UTC 2019 *)
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.

(* Fri Mar 15 15:02:15 UTC 2019 *)
(* Fri Mar 15 16:36:36 UTC 2019 *)
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;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:04&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:27&nbsp;UTC&nbsp;2019&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.
(** [] *)

(* Fri Mar 15 15:02:04 UTC 2019 *)
(* Fri Mar 15 16:36:27 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/RelTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* Fri Mar 15 15:02:16 UTC 2019 *)
(* Fri Mar 15 16:36:38 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/Tactics.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1634,7 +1634,7 @@ <h1 class="libtitle">Tactics<span class="subtitle">更多基本策略</span></h1
<span class="proofbox">&#9744;</span>
<div class="code code-tight">

<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;15:02:03&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;Fri&nbsp;Mar&nbsp;15&nbsp;16:36:26&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>

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



(* Fri Mar 15 15:02:03 UTC 2019 *)
(* Fri Mar 15 16:36:26 UTC 2019 *)
2 changes: 1 addition & 1 deletion lf-current/TacticsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,4 +219,4 @@ idtac "---------- existsb_existsb' ---------".
Print Assumptions existsb_existsb'.
Abort.

(* Fri Mar 15 15:02:10 UTC 2019 *)
(* Fri Mar 15 16:36:32 UTC 2019 *)
Binary file modified lf-current/lf.tgz
View file
Binary file not shown.
Loading

0 comments on commit a58f574

Please sign in to comment.