Add info about transitioning to standard Lean

IntroLean.qmd

@@ -15,7 +15,7 @@ Suppose $P \to (Q \to R)$.  Then $\neg R \to (P \to \neg Q)$.
 Suppose $\neg R$.  Suppose $P$.  Since $P$ and $P \to (Q \to R)$, it follows that $Q \to R$.  But then, since $\neg R$, we can conclude $\neg Q$.  Thus, $P \to \neg Q$.  Therefore $\neg R \to (P \to \neg Q)$. [ □]{.excl}\qedhere
 :::
 
-And here is how we would write the proof in Lean.^[Experienced Lean users will notice that the Lean proofs in this book look somewhat different from standard Lean proofs.  This is because our proofs use a number of custom tactics.  These tactics are designed to make our Lean proofs more readable and to bring Lean into closer agreement with *HTPI*.  These custom tactics are defined in the file "HTPIDefs.lean", which is in the folder "HTPILib" in the Lean package that accompanies this book.  The appendix includes advice about transitioning from the Lean in this book to standard Lean.]  (If you are reading this book online, then Lean examples like the one below will appear in gray boxes.  You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)
+And here is how we would write the proof in Lean.^[Experienced Lean users will notice that the Lean proofs in this book look somewhat different from standard Lean proofs.  This is because our proofs use a number of custom tactics.  These tactics are designed to make our Lean proofs more readable and to bring Lean into closer agreement with *HTPI*.  The custom tactics are defined in the file "HTPIDefs.lean", which is in the folder "HTPILib" in the Lean package that accompanies this book.  The appendix of this book includes [advice about transitioning from the Lean in this book to standard Lean](#transitioning-to-standard-lean).]  (If you are reading this book online, then Lean examples like the one below will appear in gray boxes.  You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)
 
 ```lean
 theorem Example_3_2_4

docs/IntroLean.html

@@ -626,7 +626,7 @@ <h2 class="anchored" data-anchor-id="types">Types</h2>
 <section id="footnotes" class="footnotes footnotes-end-of-document" role="doc-endnotes">
 <hr>
 <ol>
-<li id="fn1"><p>Experienced Lean users will notice that the Lean proofs in this book look somewhat different from standard Lean proofs. This is because our proofs use a number of custom tactics. These tactics are designed to make our Lean proofs more readable and to bring Lean into closer agreement with <em>HTPI</em>. These custom tactics are defined in the file “HTPIDefs.lean”, which is in the folder “HTPILib” in the Lean package that accompanies this book. The appendix includes advice about transitioning from the Lean in this book to standard Lean.<a href="#fnref1" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
+<li id="fn1"><p>Experienced Lean users will notice that the Lean proofs in this book look somewhat different from standard Lean proofs. This is because our proofs use a number of custom tactics. These tactics are designed to make our Lean proofs more readable and to bring Lean into closer agreement with <em>HTPI</em>. The custom tactics are defined in the file “HTPIDefs.lean”, which is in the folder “HTPILib” in the Lean package that accompanies this book. The appendix of this book includes <a href="Appendix.html#transitioning-to-standard-lean">advice about transitioning from the Lean in this book to standard Lean</a>.<a href="#fnref1" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
 </ol>
 </section>
 

docs/index.html

@@ -229,7 +229,7 @@ <h2 class="anchored" data-anchor-id="about-this-book">About This Book</h2>
 <h2 class="anchored" data-anchor-id="about-lean">About Lean</h2>
 <p><a href="https://leanprover.github.io">Lean</a> is a kind of software package called a <em>proof assistant</em>. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.</p>
 <p>Of course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.</p>
-<p>Note that this book uses a customized version of Lean. The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with <em>HTPI</em>. The appendix includes advice about transitioning from the Lean in this book to standard Lean.</p>
+<p>Note that this book uses a customized version of Lean. The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with <em>HTPI</em>. The appendix of this book includes <a href="Appendix.html#transitioning-to-standard-lean">advice about transitioning from the Lean in this book to standard Lean</a>.</p>
 </section>
 <section id="installing-lean" class="level2">
 <h2 class="anchored" data-anchor-id="installing-lean">Installing Lean</h2>

docs/search.json

@@ -18,7 +18,7 @@
     "href": "index.html#about-lean",
     "title": "How To Prove It With Lean",
     "section": "About Lean",
-    "text": "About Lean\nLean is a kind of software package called a proof assistant. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.\nOf course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.\nNote that this book uses a customized version of Lean. The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with HTPI. The appendix includes advice about transitioning from the Lean in this book to standard Lean."
+    "text": "About Lean\nLean is a kind of software package called a proof assistant. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.\nOf course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.\nNote that this book uses a customized version of Lean. The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with HTPI. The appendix of this book includes advice about transitioning from the Lean in this book to standard Lean."
   },
   {
     "objectID": "index.html#installing-lean",

index.qmd

@@ -18,7 +18,7 @@ If you are reading this book online, then at the end of the title in the left ma
 
 Of course, to make this possible, you must type your proof in a format that Lean understands.  Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.
 
-Note that this book uses a customized version of Lean.  The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with *HTPI*.  The appendix includes advice about transitioning from the Lean in this book to standard Lean.
+Note that this book uses a customized version of Lean.  The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with *HTPI*.  The appendix of this book includes [advice about transitioning from the Lean in this book to standard Lean](#transitioning-to-standard-lean).
 
 ## Installing Lean