From 08de7b3706ae9dbc0256dc9f44748486f9183edc Mon Sep 17 00:00:00 2001
From: djvelleman <110697570+djvelleman@users.noreply.github.com>
Date: Fri, 29 Nov 2024 11:42:37 -0500
Subject: [PATCH] Add info about transitioning to standard Lean
---
IntroLean.qmd | 2 +-
docs/IntroLean.html | 2 +-
docs/index.html | 2 +-
docs/search.json | 2 +-
index.qmd | 2 +-
5 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/IntroLean.qmd b/IntroLean.qmd
index b66f479..7d1fc19 100644
--- a/IntroLean.qmd
+++ b/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
diff --git a/docs/IntroLean.html b/docs/IntroLean.html
index 714da84..ffc8ec5 100644
--- a/docs/IntroLean.html
+++ b/docs/IntroLean.html
@@ -626,7 +626,7 @@ Types
diff --git a/docs/index.html b/docs/index.html
index a3ca38d..5895dd1 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -229,7 +229,7 @@ About This Book
About Lean
Lean 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.
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.
Installing Lean
diff --git a/docs/search.json b/docs/search.json
index 9fbebd9..4d6a184 100644
--- a/docs/search.json
+++ b/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",
diff --git a/index.qmd b/index.qmd
index 7994fb4..c877586 100644
--- a/index.qmd
+++ b/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