Update instructions for toggling infoview

IntroLean.qmd

@@ -58,7 +58,7 @@ We can learn something else from this example by changing it slightly.  If you c
 theorem extremely_easy (P : Prop) (h : P) : P := **f::
 ```
 
-This indicates that Lean has detected an error in the proof.  Lean always indicates errors by putting a red squiggle under the offending text.  Lean also puts a message in the Lean Infoview pane explaining what the error is.  (If you don't see the Infoview pane, choose "Command Palette ..." in the "View" menu, and then type "Lean" in the text box that appears.  You will see a list of commands that start with "Lean".  Click on "Lean 4: Infoview: Toggle" to make the Infoview pane appear.)  In this case, the message is `unknown identifier 'f'`.  The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears.  If you change `f` back to `h`, the red squiggle and error message go away.
+This indicates that Lean has detected an error in the proof.  Lean always indicates errors by putting a red squiggle under the offending text.  Lean also puts a message in the Lean Infoview pane explaining what the error is.  (If you don't see the Infoview pane on the right side of the window, click on the "$\forall$" icon near the top of the window and select "Infoview: Toggle Infoview" from the popup menu to make the Infoview pane appear.)  In this case, the message is `unknown identifier 'f'`.  The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears.  If you change `f` back to `h`, the red squiggle and error message go away.
 
 Let's try a slightly less trivial example.  You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate.  To type the `→` symbol in the next example, type `\to` and then hit either the space bar or the tab key; when you type either space or tab, the `\to` will change to `→`.  Alternatively, you can type `\r` (short for "right arrow") or `\imp` (short for "implies"), again followed by either space or tab.  Or, you can type `->`, and Lean will interpret it as `→`.  (There is a list in the appendix showing how to type all of the symbols used in this book.)
 

docs/IntroLean.html

@@ -291,7 +291,7 @@ <h2 class="anchored" data-anchor-id="term-mode">Term Mode</h2>
 <p>Even though this example is a triviality, there are some things to be learned from it. First of all, although we have been describing the letter <code>h</code> as an <em>identifier</em> for the hypothesis <code>P</code>, this example illustrates that Lean also considers <code>h</code> to be a <em>proof</em> of <code>P</code>. In general, when we see <code>h : P</code> in a Lean proof, where <code>P</code> is a proposition, we can think of it as meaning, not just that <code>h</code> is an identifier for the statement <code>P</code>, but also that <code>h</code> is a proof of <code>P</code>.</p>
 <p>We can learn something else from this example by changing it slightly. If you change the final <code>h</code> to a different letter—say, <code>f</code>—you will see that Lean puts a red squiggly line under the <code>f</code>, like this:</p>
 <div class="sourceCode" id="cb3"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb3-1"><a href="#cb3-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> extremely_easy (P : <span class="kw">Prop</span>) (h : P) : P := <span class="sc">**</span><span class="er">f</span><span class="sc">::</span></span></code><button title="Copy to Clipboard" class="code-copy-button"><i class="bi"></i></button></pre></div>
-<p>This indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane, choose “Command Palette …” in the “View” menu, and then type “Lean” in the text box that appears. You will see a list of commands that start with “Lean”. Click on “Lean 4: Infoview: Toggle” to make the Infoview pane appear.) In this case, the message is <code>unknown identifier 'f'</code>. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change <code>f</code> back to <code>h</code>, the red squiggle and error message go away.</p>
+<p>This indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane on the right side of the window, click on the “<span class="math inline">\(\forall\)</span>” icon near the top of the window and select “Infoview: Toggle Infoview” from the popup menu to make the Infoview pane appear.) In this case, the message is <code>unknown identifier 'f'</code>. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change <code>f</code> back to <code>h</code>, the red squiggle and error message go away.</p>
 <p>Let’s try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the <code>→</code> symbol in the next example, type <code>\to</code> and then hit either the space bar or the tab key; when you type either space or tab, the <code>\to</code> will change to <code>→</code>. Alternatively, you can type <code>\r</code> (short for “right arrow”) or <code>\imp</code> (short for “implies”), again followed by either space or tab. Or, you can type <code>-&gt;</code>, and Lean will interpret it as <code>→</code>. (There is a list in the appendix showing how to type all of the symbols used in this book.)</p>
 <div class="sourceCode" id="cb4"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb4-1"><a href="#cb4-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> very_easy</span>
 <span id="cb4-2"><a href="#cb4-2" aria-hidden="true" tabindex="-1"></a>    (P Q : <span class="kw">Prop</span>) (h1 : P → Q) (h2 : P) : Q := h1 h2</span></code><button title="Copy to Clipboard" class="code-copy-button"><i class="bi"></i></button></pre></div>

docs/search.json

@@ -88,7 +88,7 @@
     "href": "IntroLean.html#term-mode",
     "title": "Introduction to Lean",
     "section": "Term Mode",
-    "text": "Term Mode\nNow that you have seen an example of a proof in Lean, it is time for you to write your first proof. Lean has two modes for writing proofs, called term mode and tactic mode. The example above was written in tactic mode, and that is the mode we will use for most proofs in this book. But before we study the construction of proofs in tactic mode, it will be helpful to learn a bit about term mode. Term mode is best for simple proofs, so we begin with a few very short proofs.\nIf you have not yet installed Lean on your computer, go back and follow the instructions for installing it now. Then in VS Code, open the folder containing the HTPI Lean Package that you downloaded, and click on the file Blank.lean. The file starts with the line import HTPILib.HTPIDefs. Click on the blank line at the end of the file; this is where you will be typing your first proofs.\nNow type in the following theorem and proof:\ntheorem extremely_easy (P : Prop) (h : P) : P := h\nThis theorem and proof are so short we have put everything on one line. In this theorem, the letter P is used to stand for a proposition. The theorem has one hypothesis, P, which has been given the identifier h, and the conclusion of the theorem is also P. The notation := indicates that what follows will be a proof in term mode.\nOf course, the proof of the theorem is extremely easy: to prove P, we just have to point out that it is given as the hypothesis h. And so the proof in Lean consists of just one letter: h.\nEven though this example is a triviality, there are some things to be learned from it. First of all, although we have been describing the letter h as an identifier for the hypothesis P, this example illustrates that Lean also considers h to be a proof of P. In general, when we see h : P in a Lean proof, where P is a proposition, we can think of it as meaning, not just that h is an identifier for the statement P, but also that h is a proof of P.\nWe can learn something else from this example by changing it slightly. If you change the final h to a different letter—say, f—you will see that Lean puts a red squiggly line under the f, like this:\ntheorem extremely_easy (P : Prop) (h : P) : P := **f::\nThis indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane, choose “Command Palette …” in the “View” menu, and then type “Lean” in the text box that appears. You will see a list of commands that start with “Lean”. Click on “Lean 4: Infoview: Toggle” to make the Infoview pane appear.) In this case, the message is unknown identifier 'f'. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change f back to h, the red squiggle and error message go away.\nLet’s try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the → symbol in the next example, type \\to and then hit either the space bar or the tab key; when you type either space or tab, the \\to will change to →. Alternatively, you can type \\r (short for “right arrow”) or \\imp (short for “implies”), again followed by either space or tab. Or, you can type ->, and Lean will interpret it as →. (There is a list in the appendix showing how to type all of the symbols used in this book.)\ntheorem very_easy\n    (P Q : Prop) (h1 : P → Q) (h2 : P) : Q := h1 h2\nIndenting the second line is not necessary, but it is traditional. When stating a theorem, we will generally indent all lines after the first with two tabs in VS Code. Once you indent a line, VS Code will maintain that same indenting in subsequent lines until you delete tabs at the beginning of a line to reduce or eliminate indenting.\nThis time there are two hypotheses, h1 : P → Q and h2 : P. As explained in Section 3.2 of HTPI, the conclusion Q follows from these hypotheses by the logical rule modus ponens. To use modus ponens to complete this proof in term mode, we simply write the identifiers of the two hypotheses—which, as we have just seen, can also be thought of as proofs of the two hypotheses—one after the other, with a space between them. It is important to write the proof of the conditional hypothesis first, so the proof is written h1 h2; if you try writing this proof as h2 h1, you will get a red squiggle. In general, if a is a proof of any conditional statement X → Y, and b is a proof of the antecedent X, then a b is a proof of the consequent Y. The proofs a and b need not be simply identifiers; any proofs of a conditional statement and its antecedent can be combined in this way.\nWe’ll try one more proof in term mode:\ntheorem easy (P Q R : Prop) (h1 : P → Q)\n    (h2 : Q → R) (h3 : P) : R :=\nNote that in the statement of the theorem, you can break the lines however you please; this time we have put the declaration of P, Q, and R and the first hypothesis on the first line and the other two hypotheses on the second line. How can we prove the conclusion R? Well, we have h2 : Q → R, so if we could prove Q then we could use modus ponens to reach the desired conclusion. In other words, h2 _ will be a proof of R, if we can fill in the blank with a proof of Q. Can we prove Q? Yes, Q follows from P → Q and P by modus ponens, so h1 h3 is a proof of Q. Filling in the blank, we conclude that h2 (h1 h3) is a proof of R. Type it in, and you’ll see that Lean will accept it. Note that the parentheses are important; if you write h2 h1 h3 then Lean will interpret it as (h2 h1) h3, which doesn’t make sense, and you’ll get an error."
+    "text": "Term Mode\nNow that you have seen an example of a proof in Lean, it is time for you to write your first proof. Lean has two modes for writing proofs, called term mode and tactic mode. The example above was written in tactic mode, and that is the mode we will use for most proofs in this book. But before we study the construction of proofs in tactic mode, it will be helpful to learn a bit about term mode. Term mode is best for simple proofs, so we begin with a few very short proofs.\nIf you have not yet installed Lean on your computer, go back and follow the instructions for installing it now. Then in VS Code, open the folder containing the HTPI Lean Package that you downloaded, and click on the file Blank.lean. The file starts with the line import HTPILib.HTPIDefs. Click on the blank line at the end of the file; this is where you will be typing your first proofs.\nNow type in the following theorem and proof:\ntheorem extremely_easy (P : Prop) (h : P) : P := h\nThis theorem and proof are so short we have put everything on one line. In this theorem, the letter P is used to stand for a proposition. The theorem has one hypothesis, P, which has been given the identifier h, and the conclusion of the theorem is also P. The notation := indicates that what follows will be a proof in term mode.\nOf course, the proof of the theorem is extremely easy: to prove P, we just have to point out that it is given as the hypothesis h. And so the proof in Lean consists of just one letter: h.\nEven though this example is a triviality, there are some things to be learned from it. First of all, although we have been describing the letter h as an identifier for the hypothesis P, this example illustrates that Lean also considers h to be a proof of P. In general, when we see h : P in a Lean proof, where P is a proposition, we can think of it as meaning, not just that h is an identifier for the statement P, but also that h is a proof of P.\nWe can learn something else from this example by changing it slightly. If you change the final h to a different letter—say, f—you will see that Lean puts a red squiggly line under the f, like this:\ntheorem extremely_easy (P : Prop) (h : P) : P := **f::\nThis indicates that Lean has detected an error in the proof. Lean always indicates errors by putting a red squiggle under the offending text. Lean also puts a message in the Lean Infoview pane explaining what the error is. (If you don’t see the Infoview pane on the right side of the window, click on the “\\(\\forall\\)” icon near the top of the window and select “Infoview: Toggle Infoview” from the popup menu to make the Infoview pane appear.) In this case, the message is unknown identifier 'f'. The message is introduced by a heading, in red, that identifies the file, the line number, and the character position on that line where the error appears. If you change f back to h, the red squiggle and error message go away.\nLet’s try a slightly less trivial example. You can type the next theorem below the previous one, leaving a blank line between them to keep them visually separate. To type the → symbol in the next example, type \\to and then hit either the space bar or the tab key; when you type either space or tab, the \\to will change to →. Alternatively, you can type \\r (short for “right arrow”) or \\imp (short for “implies”), again followed by either space or tab. Or, you can type ->, and Lean will interpret it as →. (There is a list in the appendix showing how to type all of the symbols used in this book.)\ntheorem very_easy\n    (P Q : Prop) (h1 : P → Q) (h2 : P) : Q := h1 h2\nIndenting the second line is not necessary, but it is traditional. When stating a theorem, we will generally indent all lines after the first with two tabs in VS Code. Once you indent a line, VS Code will maintain that same indenting in subsequent lines until you delete tabs at the beginning of a line to reduce or eliminate indenting.\nThis time there are two hypotheses, h1 : P → Q and h2 : P. As explained in Section 3.2 of HTPI, the conclusion Q follows from these hypotheses by the logical rule modus ponens. To use modus ponens to complete this proof in term mode, we simply write the identifiers of the two hypotheses—which, as we have just seen, can also be thought of as proofs of the two hypotheses—one after the other, with a space between them. It is important to write the proof of the conditional hypothesis first, so the proof is written h1 h2; if you try writing this proof as h2 h1, you will get a red squiggle. In general, if a is a proof of any conditional statement X → Y, and b is a proof of the antecedent X, then a b is a proof of the consequent Y. The proofs a and b need not be simply identifiers; any proofs of a conditional statement and its antecedent can be combined in this way.\nWe’ll try one more proof in term mode:\ntheorem easy (P Q R : Prop) (h1 : P → Q)\n    (h2 : Q → R) (h3 : P) : R :=\nNote that in the statement of the theorem, you can break the lines however you please; this time we have put the declaration of P, Q, and R and the first hypothesis on the first line and the other two hypotheses on the second line. How can we prove the conclusion R? Well, we have h2 : Q → R, so if we could prove Q then we could use modus ponens to reach the desired conclusion. In other words, h2 _ will be a proof of R, if we can fill in the blank with a proof of Q. Can we prove Q? Yes, Q follows from P → Q and P by modus ponens, so h1 h3 is a proof of Q. Filling in the blank, we conclude that h2 (h1 h3) is a proof of R. Type it in, and you’ll see that Lean will accept it. Note that the parentheses are important; if you write h2 h1 h3 then Lean will interpret it as (h2 h1) h3, which doesn’t make sense, and you’ll get an error."
   },
   {
     "objectID": "IntroLean.html#tactic-mode",