r4240

lf-current/AltAuto.html

@@ -2417,7 +2417,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/AltAuto.v

@@ -1832,4 +1832,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
 
     - Ltac functions and [match goal] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/AltAutoTest.v

@@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Auto.html

@@ -910,7 +910,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
 <span class="id" title="keyword">Proof</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">HP</span> <span class="id" title="var">HQ</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">HP</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">y</span> <span class="id" title="var">HP'</span>]. <span class="id" title="tactic">eauto</span>.<br/>
 <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Auto.v

@@ -740,4 +740,4 @@ Proof.
   intros P Q HP HQ. destruct HP as [y HP']. eauto.
 Qed.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/AutoTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Basics.html

@@ -2691,7 +2691,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Functional Programming in Coq<
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Basics.v

@@ -2015,4 +2015,4 @@ Example test_bin_incr6 :
     output.  But since they have to be graded by a human, the test
     script won't be able to tell you much about them.  *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/BasicsTest.v

@@ -521,4 +521,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Bib.html

@@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Bib.v

@@ -32,4 +32,4 @@
 
 *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/BibTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Extraction.html

@@ -232,7 +232,7 @@ <h1 class="libtitle">Extraction<span class="subtitle">Extracting OCaml from Coq<
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Extraction.v

@@ -129,4 +129,4 @@ Extraction "imp.ml" empty_st ceval_step parse.
     chapter in _Verified Functional Algorithms_ (_Software
     Foundations_ volume 3). *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ExtractionTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Imp.html

@@ -2861,7 +2861,7 @@ <h1 class="libtitle">Imp<span class="subtitle">Simple Imperative Programs</span>
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Imp.v

@@ -2077,4 +2077,4 @@ End BreakImp.
 
     [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ImpCEvalFun.html

@@ -481,7 +481,7 @@ <h1 class="libtitle">ImpCEvalFun<span class="subtitle">An Evaluation Function fo
 </div>
 
 <br/>
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/ImpCEvalFun.v

@@ -393,4 +393,4 @@ Proof.
   rewrite E1 in E2. inversion E2. reflexivity.
   lia. lia.  Qed.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ImpCEvalFunTest.v

@@ -91,4 +91,4 @@ idtac "---------- ceval_step__ceval_inf ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ImpParser.html

@@ -536,7 +536,7 @@ <h1 class="libtitle">ImpParser<span class="subtitle">Lexing and Parsing in Coq</
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">end</span></a><a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "z" <a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a>.<br/>
 <span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">cbv</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/ImpParser.v

@@ -462,4 +462,4 @@ Example eg2 : parse "
       "x" := "z" }>.
 Proof. cbv. reflexivity. Qed.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ImpParserTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ImpTest.v

@@ -314,4 +314,4 @@ idtac "---------- BreakImp.seq_stops_on_break ---------".
 Print Assumptions BreakImp.seq_stops_on_break.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/IndPrinciples.html

@@ -1361,7 +1361,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">Induction Principles</s
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/IndPrinciples.v

@@ -963,4 +963,4 @@ Proof. (* FILL IN HERE *) Admitted.
 
 (** [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/IndPrinciplesTest.v

@@ -109,4 +109,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/IndProp.html

@@ -3320,7 +3320,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">Inductively Defined Propositi
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/IndProp.v

@@ -2433,4 +2433,4 @@ Proof.
   (* FILL IN HERE *) Admitted.
 (** [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/IndPropTest.v

@@ -332,4 +332,4 @@ idtac "---------- merge_filter ---------".
 Print Assumptions merge_filter.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Induction.html

@@ -1115,7 +1115,7 @@ <h1 class="libtitle">Induction<span class="subtitle">Proof by Induction</span></
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Induction.v

@@ -792,4 +792,4 @@ Proof.
 
 (** [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/InductionTest.v

@@ -258,4 +258,4 @@ idtac "---------- bin_nat_bin ---------".
 Print Assumptions bin_nat_bin.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Lists.html

@@ -1522,7 +1522,7 @@ <h1 class="libtitle">Lists<span class="subtitle">Working with Structured Data</s
 
 <div class="code">
 <span class="id" title="keyword">End</span> <a class="idref" href="Lists.html#PartialMap"><span class="id" title="module">PartialMap</span></a>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Lists.v

@@ -1137,4 +1137,4 @@ Proof.
 (** [] *)
 End PartialMap.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/ListsTest.v

@@ -516,4 +516,4 @@ idtac "---------- NatList.rev_injective ---------".
 Print Assumptions NatList.rev_injective.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Logic.html

@@ -2424,7 +2424,7 @@ <h1 class="libtitle">Logic<span class="subtitle">Logic in Coq</span></h1>
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Logic.v

@@ -1745,4 +1745,4 @@ Definition consequentia_mirabilis := forall P:Prop,
 
     [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/LogicTest.v

@@ -414,4 +414,4 @@ idtac "---------- not_exists_dist ---------".
 Print Assumptions not_exists_dist.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Maps.html

@@ -562,7 +562,7 @@ <h1 class="libtitle">Maps<span class="subtitle">Total and Partial Maps</span></h
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Maps.v

@@ -379,4 +379,4 @@ Qed.
     used to keep track of which program variables are defined in a
     given scope. *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/MapsTest.v

@@ -94,4 +94,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Poly.html

@@ -1735,7 +1735,7 @@ <h1 class="libtitle">Poly<span class="subtitle">Polymorphism and Higher-Order Fu
 
 <span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises.Church"><span class="id" title="module">Church</span></a>.<br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises"><span class="id" title="module">Exercises</span></a>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Poly.v

@@ -1224,4 +1224,4 @@ Proof. (* FILL IN HERE *) Admitted.
 End Church.
 End Exercises.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/PolyTest.v

@@ -498,4 +498,4 @@ idtac "---------- Exercises.Church.exp_3 ---------".
 Print Assumptions Exercises.Church.exp_3.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Postscript.html

@@ -217,7 +217,7 @@ <h1 class="libtitle">Postscript</h1>
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Postscript.v

@@ -82,4 +82,4 @@
          {https://deepspec.org/event/dsss17/index.html}
 *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/PostscriptTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Preface.html

@@ -757,7 +757,7 @@ <h1 class="libtitle">Preface</h1>
 </div>
 <div class="code">
 <br/>
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:57&nbsp;*)</span><br/>
 </span></div>
 </div>
 

lf-current/Preface.v

@@ -508,4 +508,4 @@
     NSF Expeditions grant 1521523, _The Science of Deep
     Specification_. *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:57 *)

lf-current/PrefaceTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ProofObjects.html

@@ -1304,7 +1304,7 @@ <h1 class="libtitle">ProofObjects<span class="subtitle">The Curry-Howard Corresp
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/ProofObjects.v

@@ -921,4 +921,4 @@ Theorem pe_implies_pi :
 Proof. (* FILL IN HERE *) Admitted.
 (** [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/ProofObjectsTest.v

@@ -345,4 +345,4 @@ idtac "---------- pe_implies_pi ---------".
 Print Assumptions pe_implies_pi.
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/Rel.html

@@ -641,7 +641,7 @@ <h1 class="libtitle">Rel<span class="subtitle">Properties of Relations</span></h
 
 <div class="code">
 
-<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-10-24&nbsp;21:58&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Rel.v

@@ -409,4 +409,4 @@ Proof.
   (* FILL IN HERE *) Admitted.
 (** [] *)
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)

lf-current/RelTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2024-10-24 21:39 *)
+(* 2024-10-24 21:58 *)