Fix typo

djvelleman · Aug 31, 2024 · 1345213 · 1345213
1 parent dde916f
commit 1345213
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 3 deletions.
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
diff --git a/docs/index.html b/docs/index.html
@@ -232,7 +232,7 @@ <h2 class="anchored" data-anchor-id="about-lean">About Lean</h2>
 </section>
 <section id="installing-lean" class="level2">
 <h2 class="anchored" data-anchor-id="installing-lean">Installing Lean</h2>
-<p>These instructions are based on the installation procedure that is describe <a href="https://lean-lang.org/lean4/doc/quickstart.html">here</a>. Alternative installation procedures can be found <a href="https://leanprover-community.github.io/get_started.html">here</a>.</p>
+<p>These instructions are based on the installation procedure that is described <a href="https://lean-lang.org/lean4/doc/quickstart.html">here</a>. Alternative installation procedures can be found <a href="https://leanprover-community.github.io/get_started.html">here</a>.</p>
 <p>We will be using Visual Studio Code to run Lean, so you will need to install VS Code first. VS Code is free and can be downloaded <a href="https://code.visualstudio.com">here</a>.</p>
 <p>You will also need the Lean package that accompanies this book, which can be downloaded from <a href="https://github.com/djvelleman/HTPILeanPackage">https://github.com/djvelleman/HTPILeanPackage</a>. After following the link, click on the green “Code” button and, in the pop-up menu, select “Download ZIP”. Open the downloaded zip file to create a folder containing the HTPI Lean package. You can put this folder wherever you want on your computer.</p>
 <p>Now open VS Code. You should see a window that looks something like this:</p>

diff --git a/docs/search.json b/docs/search.json
@@ -25,7 +25,7 @@
     "href": "index.html#installing-lean",
     "title": "How To Prove It With Lean",
     "section": "Installing Lean",
-    "text": "Installing Lean\nThese instructions are based on the installation procedure that is describe here. Alternative installation procedures can be found here.\nWe will be using Visual Studio Code to run Lean, so you will need to install VS Code first. VS Code is free and can be downloaded here.\nYou will also need the Lean package that accompanies this book, which can be downloaded from https://github.com/djvelleman/HTPILeanPackage. After following the link, click on the green “Code” button and, in the pop-up menu, select “Download ZIP”. Open the downloaded zip file to create a folder containing the HTPI Lean package. You can put this folder wherever you want on your computer.\nNow open VS Code. You should see a window that looks something like this:\n\nClick on the Extensions icon on the left side of the window, which is circled in red in the image above. That will bring up a list of available extensions:\n\nIn the Search Extensions in Marketplace field, type “lean4”. VS Code should find the Lean 4 extension and display it:\n\nClick on “Install” to install the Lean 4 extension.\nNext, in VS Code, select “Open Folder …” from the File menu and open the folder containing the HTPI Lean package that you downloaded earlier. Under the heading “Explorer” on the left side of the window, you should see a list of the files in the package. (If you don’t see the list, try clicking on the Explorer icon, circled in red below.)\n\nClick on the file “Blank.lean” in the file list. You should see a warning that VS Code failed to start the ‘lean’ language server:\n\n\n\n\n\nClick on the “Install Lean using Elan” button, and Lean should be installed. Then Lean should “build” the HTPI Lean package. This may take a while, but it only has to be done once.\nIf anything goes wrong, try quitting VS Code and restarting. Eventually your window should look like this:\n\nIf you don’t see the Infoview pane on the right side of the window, click on the “\\(\\forall\\)” icon circled in red in the image above and select “Infoview: Toggle Infoview” from the popup menu.\nYour installation is now complete."
+    "text": "Installing Lean\nThese instructions are based on the installation procedure that is described here. Alternative installation procedures can be found here.\nWe will be using Visual Studio Code to run Lean, so you will need to install VS Code first. VS Code is free and can be downloaded here.\nYou will also need the Lean package that accompanies this book, which can be downloaded from https://github.com/djvelleman/HTPILeanPackage. After following the link, click on the green “Code” button and, in the pop-up menu, select “Download ZIP”. Open the downloaded zip file to create a folder containing the HTPI Lean package. You can put this folder wherever you want on your computer.\nNow open VS Code. You should see a window that looks something like this:\n\nClick on the Extensions icon on the left side of the window, which is circled in red in the image above. That will bring up a list of available extensions:\n\nIn the Search Extensions in Marketplace field, type “lean4”. VS Code should find the Lean 4 extension and display it:\n\nClick on “Install” to install the Lean 4 extension.\nNext, in VS Code, select “Open Folder …” from the File menu and open the folder containing the HTPI Lean package that you downloaded earlier. Under the heading “Explorer” on the left side of the window, you should see a list of the files in the package. (If you don’t see the list, try clicking on the Explorer icon, circled in red below.)\n\nClick on the file “Blank.lean” in the file list. You should see a warning that VS Code failed to start the ‘lean’ language server:\n\n\n\n\n\nClick on the “Install Lean using Elan” button, and Lean should be installed. Then Lean should “build” the HTPI Lean package. This may take a while, but it only has to be done once.\nIf anything goes wrong, try quitting VS Code and restarting. Eventually your window should look like this:\n\nIf you don’t see the Infoview pane on the right side of the window, click on the “\\(\\forall\\)” icon circled in red in the image above and select “Infoview: Toggle Infoview” from the popup menu.\nYour installation is now complete."
   },
   {
     "objectID": "index.html#using-gitpod",

diff --git a/index.qmd b/index.qmd
@@ -20,7 +20,7 @@ Of course, to make this possible, you must type your proof in a format that Lean
 
 ## Installing Lean
 
-These instructions are based on the installation procedure that is describe [here](https://lean-lang.org/lean4/doc/quickstart.html).  Alternative installation procedures can be found [here](https://leanprover-community.github.io/get_started.html).
+These instructions are based on the installation procedure that is described [here](https://lean-lang.org/lean4/doc/quickstart.html).  Alternative installation procedures can be found [here](https://leanprover-community.github.io/get_started.html).
 
 We will be using Visual Studio Code to run Lean, so you will need to install VS Code first.  VS Code is free and can be downloaded [here](https://code.visualstudio.com).