Skip to content

Commit

Permalink
r4239
Browse files Browse the repository at this point in the history
  • Loading branch information
@bcpierce00
bcpierce00 committed Oct 24, 2024
1 parent dc7ee21 commit 20a2802
Show file tree
Hide file tree
Showing 346 changed files with 382 additions and 382 deletions.
14 changes: 7 additions & 7 deletions common/css/sf.css
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ ul#menu li, div.button {
display: inline-block;
background-color: white;
padding: 5px;
font-size: .70em;
font-size: .80em;
text-transform: uppercase;
width: 30%;
text-align: center;
Expand Down Expand Up @@ -188,7 +188,7 @@ h4.section {

#main .doc {
margin: 0px auto;
font-size: 14px;
font-size: 16px;
line-height: 22px;
/* max-width: 570px; */
color: black;
Expand Down Expand Up @@ -254,7 +254,7 @@ h1 .inlinecode .id, h1.section span.inlinecode {

.doc .code {
display: inline;
font-size: 110%;
font-size: 120%;
color: rgb(35%,35%,70%);
font-family: monospace;
padding-left: 0px;
Expand Down Expand Up @@ -360,7 +360,7 @@ div.hidden {

.code {
padding-left: 20px;
font-size: 14px;
font-size: 110%;
font-family: monospace;
line-height: 17px;
margin-top: 9px;
Expand Down Expand Up @@ -394,7 +394,7 @@ div.hidden {
hr.doublespaceincode {
height: 1pt;
visibility: hidden;
font-size: 10px;
font-size: 12px;
}

/*
Expand Down Expand Up @@ -568,7 +568,7 @@ div#sec1.hide { display: none; }

#toc ul {
padding-top: 8px;
font-size: 14px;
font-size: 16px;
padding-left: 0;
}

Expand Down Expand Up @@ -997,7 +997,7 @@ body.sf_home #main_home {
background-color: transparent;
}

/* A partial fix to a coqdoc bug...
/* A partial fix to a coqdoc bug...
See https://github.com/DeepSpec/sfdev/issues/236 */
.inlinecode { white-space: pre; }
.inlinecode br { display: none; }
2 changes: 1 addition & 1 deletion lf-current/AltAuto.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/AltAuto.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1832,4 +1832,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
- Ltac functions and [match goal] *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/AltAutoTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------".
idtac "MANUAL".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Auto.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -740,4 +740,4 @@ Proof.
intros P Q HP HQ. destruct HP as [y HP']. eauto.
Qed.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/AutoTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Basics.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -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-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/BasicsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -521,4 +521,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
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">Bibliography</span></h1>
</div>
<div class="code">

<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@
*)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/BibTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Extraction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -129,4 +129,4 @@ Extraction "imp.ml" empty_st ceval_step parse.
chapter in _Verified Functional Algorithms_ (_Software
Foundations_ volume 3). *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ExtractionTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Imp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2861,7 +2861,7 @@ <h1 class="libtitle">Imp<span class="subtitle">Simple Imperative Programs</span>

<div class="code">

<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -2077,4 +2077,4 @@ End BreakImp.

[] *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFun.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -481,7 +481,7 @@ <h1 class="libtitle">ImpCEvalFun<span class="subtitle">An Evaluation Function fo
</div>

<br/>
<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -393,4 +393,4 @@ Proof.
rewrite E1 in E2. inversion E2. reflexivity.
lia. lia. Qed.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFunTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,4 +91,4 @@ idtac "---------- ceval_step__ceval_inf ---------".
idtac "MANUAL".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ImpParser.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -462,4 +462,4 @@ Example eg2 : parse "
"x" := "z" }>.
Proof. cbv. reflexivity. Qed.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ImpParserTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ImpTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -314,4 +314,4 @@ idtac "---------- BreakImp.seq_stops_on_break ---------".
Print Assumptions BreakImp.seq_stops_on_break.
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/IndPrinciples.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1361,7 +1361,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">Induction Principles</s

<div class="code">

<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -963,4 +963,4 @@ Proof. (* FILL IN HERE *) Admitted.

(** [] *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/IndPrinciplesTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,4 +109,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/IndProp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3320,7 +3320,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">Inductively Defined Propositi

<div class="code">

<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -2433,4 +2433,4 @@ Proof.
(* FILL IN HERE *) Admitted.
(** [] *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/IndPropTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -332,4 +332,4 @@ idtac "---------- merge_filter ---------".
Print Assumptions merge_filter.
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Induction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1115,7 +1115,7 @@ <h1 class="libtitle">Induction<span class="subtitle">Proof by Induction</span></

<div class="code">

<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -792,4 +792,4 @@ Proof.

(** [] *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/InductionTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -258,4 +258,4 @@ idtac "---------- bin_nat_bin ---------".
Print Assumptions bin_nat_bin.
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Lists.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -1137,4 +1137,4 @@ Proof.
(** [] *)
End PartialMap.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/ListsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -516,4 +516,4 @@ idtac "---------- NatList.rev_injective ---------".
Print Assumptions NatList.rev_injective.
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Logic.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -1745,4 +1745,4 @@ Definition consequentia_mirabilis := forall P:Prop,

[] *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/LogicTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -414,4 +414,4 @@ idtac "---------- not_exists_dist ---------".
Print Assumptions not_exists_dist.
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Maps.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -379,4 +379,4 @@ Qed.
used to keep track of which program variables are defined in a
given scope. *)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/MapsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,4 +94,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Poly.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -1224,4 +1224,4 @@ Proof. (* FILL IN HERE *) Admitted.
End Church.
End Exercises.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/PolyTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -498,4 +498,4 @@ idtac "---------- Exercises.Church.exp_3 ---------".
Print Assumptions Exercises.Church.exp_3.
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/Postscript.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ <h1 class="libtitle">Postscript</h1>
</div>
<div class="code">

<span class="comment">(*&nbsp;2024-10-04&nbsp;13:52&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-10-24&nbsp;21:39&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 @@ -82,4 +82,4 @@
{https://deepspec.org/event/dsss17/index.html}
*)

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
2 changes: 1 addition & 1 deletion lf-current/PostscriptTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2024-10-04 13:52 *)
(* 2024-10-24 21:39 *)
Loading

0 comments on commit 20a2802

Please sign in to comment.