Add "decide" to list of keywords to highlight

docs/Chap6.html

@@ -480,7 +480,7 @@ <h4 class="anchored" data-anchor-id="to-prove-a-goal-of-the-form-n-nat-p-n">To p
 <div class="sourceCode" id="cb18"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb18-1"><a href="#cb18-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> Example_6_1_3 : ∀ n ≥ 5, 2 ^ n &gt; n ^ 2 := <span class="kw">by</span></span>
 <span id="cb18-2"><a href="#cb18-2" aria-hidden="true" tabindex="-1"></a>  <span class="kw">by_induc</span></span>
 <span id="cb18-3"><a href="#cb18-3" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Base Case</span></span>
-<span id="cb18-4"><a href="#cb18-4" aria-hidden="true" tabindex="-1"></a>    decide</span>
+<span id="cb18-4"><a href="#cb18-4" aria-hidden="true" tabindex="-1"></a>    <span class="kw">decide</span></span>
 <span id="cb18-5"><a href="#cb18-5" aria-hidden="true" tabindex="-1"></a>    <span class="kw">done</span></span>
 <span id="cb18-6"><a href="#cb18-6" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Induction Step</span></span>
 <span id="cb18-7"><a href="#cb18-7" aria-hidden="true" tabindex="-1"></a>    <span class="kw">fix</span> n : Nat</span>
@@ -877,7 +877,7 @@ <h2 class="anchored" data-anchor-id="recursion">6.3. Recursion</h2>
 <div class="sourceCode" id="cb54"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb54-1"><a href="#cb54-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> <span class="sc">??</span><span class="an">Example_6_3_1</span><span class="sc">::</span> : ∀ n ≥ 4, fact n &gt; 2 ^ n := <span class="kw">by</span></span>
 <span id="cb54-2"><a href="#cb54-2" aria-hidden="true" tabindex="-1"></a>  <span class="kw">by_induc</span></span>
 <span id="cb54-3"><a href="#cb54-3" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Base Case</span></span>
-<span id="cb54-4"><a href="#cb54-4" aria-hidden="true" tabindex="-1"></a>    decide</span>
+<span id="cb54-4"><a href="#cb54-4" aria-hidden="true" tabindex="-1"></a>    <span class="kw">decide</span></span>
 <span id="cb54-5"><a href="#cb54-5" aria-hidden="true" tabindex="-1"></a>    <span class="kw">done</span></span>
 <span id="cb54-6"><a href="#cb54-6" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Induction Step</span></span>
 <span id="cb54-7"><a href="#cb54-7" aria-hidden="true" tabindex="-1"></a>    <span class="kw">fix</span> n : Nat</span>
@@ -910,7 +910,7 @@ <h2 class="anchored" data-anchor-id="recursion">6.3. Recursion</h2>
 <div class="sourceCode" id="cb58"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb58-1"><a href="#cb58-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> Example_6_3_1 : ∀ n ≥ 4, fact n &gt; 2 ^ n := <span class="kw">by</span></span>
 <span id="cb58-2"><a href="#cb58-2" aria-hidden="true" tabindex="-1"></a>  <span class="kw">by_induc</span></span>
 <span id="cb58-3"><a href="#cb58-3" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Base Case</span></span>
-<span id="cb58-4"><a href="#cb58-4" aria-hidden="true" tabindex="-1"></a>    decide</span>
+<span id="cb58-4"><a href="#cb58-4" aria-hidden="true" tabindex="-1"></a>    <span class="kw">decide</span></span>
 <span id="cb58-5"><a href="#cb58-5" aria-hidden="true" tabindex="-1"></a>    <span class="kw">done</span></span>
 <span id="cb58-6"><a href="#cb58-6" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Induction Step</span></span>
 <span id="cb58-7"><a href="#cb58-7" aria-hidden="true" tabindex="-1"></a>    <span class="kw">fix</span> n : Nat</span>
@@ -932,7 +932,7 @@ <h2 class="anchored" data-anchor-id="recursion">6.3. Recursion</h2>
 <div class="sourceCode" id="cb59"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb59-1"><a href="#cb59-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> Example_6_3_1 : ∀ n ≥ 4, fact n &gt; 2 ^ n := <span class="kw">by</span></span>
 <span id="cb59-2"><a href="#cb59-2" aria-hidden="true" tabindex="-1"></a>  <span class="kw">by_induc</span></span>
 <span id="cb59-3"><a href="#cb59-3" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Base Case</span></span>
-<span id="cb59-4"><a href="#cb59-4" aria-hidden="true" tabindex="-1"></a>    decide</span>
+<span id="cb59-4"><a href="#cb59-4" aria-hidden="true" tabindex="-1"></a>    <span class="kw">decide</span></span>
 <span id="cb59-5"><a href="#cb59-5" aria-hidden="true" tabindex="-1"></a>    <span class="kw">done</span></span>
 <span id="cb59-6"><a href="#cb59-6" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Induction Step</span></span>
 <span id="cb59-7"><a href="#cb59-7" aria-hidden="true" tabindex="-1"></a>    <span class="kw">fix</span> n : Nat</span>
@@ -1321,13 +1321,13 @@ <h4 class="anchored" data-anchor-id="to-prove-a-goal-of-the-form-n-nat-p-n-1">To
 <span id="cb94-5"><a href="#cb94-5" aria-hidden="true" tabindex="-1"></a>  <span class="kw">by_cases</span> h1 : n = 0</span>
 <span id="cb94-6"><a href="#cb94-6" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Case 1. h1 : n = 0</span></span>
 <span id="cb94-7"><a href="#cb94-7" aria-hidden="true" tabindex="-1"></a>    <span class="kw">rewrite</span> [h1]   <span class="co">--Goal : Fib 0 &lt; 2 ^ 0</span></span>
-<span id="cb94-8"><a href="#cb94-8" aria-hidden="true" tabindex="-1"></a>    decide</span>
+<span id="cb94-8"><a href="#cb94-8" aria-hidden="true" tabindex="-1"></a>    <span class="kw">decide</span></span>
 <span id="cb94-9"><a href="#cb94-9" aria-hidden="true" tabindex="-1"></a>    <span class="kw">done</span></span>
 <span id="cb94-10"><a href="#cb94-10" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- Case 2. h1 : ¬n = 0</span></span>
 <span id="cb94-11"><a href="#cb94-11" aria-hidden="true" tabindex="-1"></a>    <span class="kw">by_cases</span> h2 : n = 1</span>
 <span id="cb94-12"><a href="#cb94-12" aria-hidden="true" tabindex="-1"></a>    · <span class="co">-- Case 2.1. h2 : n = 1</span></span>
 <span id="cb94-13"><a href="#cb94-13" aria-hidden="true" tabindex="-1"></a>      <span class="kw">rewrite</span> [h2]</span>
-<span id="cb94-14"><a href="#cb94-14" aria-hidden="true" tabindex="-1"></a>      decide</span>
+<span id="cb94-14"><a href="#cb94-14" aria-hidden="true" tabindex="-1"></a>      <span class="kw">decide</span></span>
 <span id="cb94-15"><a href="#cb94-15" aria-hidden="true" tabindex="-1"></a>      <span class="kw">done</span></span>
 <span id="cb94-16"><a href="#cb94-16" aria-hidden="true" tabindex="-1"></a>    · <span class="co">-- Case 2.2. h2 : ¬n = 1</span></span>
 <span id="cb94-17"><a href="#cb94-17" aria-hidden="true" tabindex="-1"></a>      <span class="kw">obtain</span> (k : Nat) (h3 : n = k + 2) <span class="kw">from</span></span>
@@ -1409,7 +1409,7 @@ <h4 class="anchored" data-anchor-id="to-prove-a-goal-of-the-form-n-nat-p-n-1">To
 <span id="cb101-19"><a href="#cb101-19" aria-hidden="true" tabindex="-1"></a>    <span class="kw">rewrite</span> [←pqsqrt2, p'halfp]</span>
 <span id="cb101-20"><a href="#cb101-20" aria-hidden="true" tabindex="-1"></a>    <span class="kw">ring</span></span>
 <span id="cb101-21"><a href="#cb101-21" aria-hidden="true" tabindex="-1"></a>    <span class="kw">done</span></span>
-<span id="cb101-22"><a href="#cb101-22" aria-hidden="true" tabindex="-1"></a>  <span class="kw">have</span> h8 : 2 &gt; 0 := <span class="kw">by</span> decide</span>
+<span id="cb101-22"><a href="#cb101-22" aria-hidden="true" tabindex="-1"></a>  <span class="kw">have</span> h8 : 2 &gt; 0 := <span class="kw">by</span> <span class="kw">decide</span></span>
 <span id="cb101-23"><a href="#cb101-23" aria-hidden="true" tabindex="-1"></a>  <span class="kw">rewrite</span> [mul_left_cancel_iff_of_pos h8] <span class="kw">at</span> h7</span>
 <span id="cb101-24"><a href="#cb101-24" aria-hidden="true" tabindex="-1"></a>    <span class="co">--h7 : 2 * (p' * p') = q * q</span></span>
 <span id="cb101-25"><a href="#cb101-25" aria-hidden="true" tabindex="-1"></a>  <span class="kw">have</span> h9 : nat_even (q * q) := Exists.intro (p' * p') h7.symm</span>

docs/Chap7.html

@@ -754,7 +754,7 @@ <h2 class="anchored" data-anchor-id="prime-factorization">7.2. Prime Factorizati
 <span id="cb35-38"><a href="#cb35-38" aria-hidden="true" tabindex="-1"></a>          _ = p * 0 := <span class="kw">by</span> <span class="kw">rw</span> [h6]</span>
 <span id="cb35-39"><a href="#cb35-39" aria-hidden="true" tabindex="-1"></a>          _ = 0 := <span class="kw">by</span> <span class="kw">ring</span></span>
 <span id="cb35-40"><a href="#cb35-40" aria-hidden="true" tabindex="-1"></a>      <span class="kw">rewrite</span> [h7]</span>
-<span id="cb35-41"><a href="#cb35-41" aria-hidden="true" tabindex="-1"></a>      decide</span>
+<span id="cb35-41"><a href="#cb35-41" aria-hidden="true" tabindex="-1"></a>      <span class="kw">decide</span></span>
 <span id="cb35-42"><a href="#cb35-42" aria-hidden="true" tabindex="-1"></a>      <span class="kw">done</span></span>
 <span id="cb35-43"><a href="#cb35-43" aria-hidden="true" tabindex="-1"></a>    <span class="kw">have</span> m_pos : 0 &lt; m := Nat.pos_of_ne_zero h5</span>
 <span id="cb35-44"><a href="#cb35-44" aria-hidden="true" tabindex="-1"></a>    <span class="kw">have</span> m_lt_n : m &lt; n := <span class="kw">by</span></span>

docs/Chap8.html

@@ -1298,7 +1298,7 @@ <h2 class="anchored" data-anchor-id="debts-paid">8.1½. Debts Paid</h2>
 <span id="cb57-18"><a href="#cb57-18" aria-hidden="true" tabindex="-1"></a>  <span class="kw">apply</span> Iff.intro</span>
 <span id="cb57-19"><a href="#cb57-19" aria-hidden="true" tabindex="-1"></a>  · <span class="co">-- (→)</span></span>
 <span id="cb57-20"><a href="#cb57-20" aria-hidden="true" tabindex="-1"></a>    <span class="kw">assume</span> h1 : numElts A 1  <span class="co">--Goal : ∃ (x : U), A = {x}</span></span>
-<span id="cb57-21"><a href="#cb57-21" aria-hidden="true" tabindex="-1"></a>    <span class="kw">have</span> h2 : 1 &gt; 0 := <span class="kw">by</span> decide</span>
+<span id="cb57-21"><a href="#cb57-21" aria-hidden="true" tabindex="-1"></a>    <span class="kw">have</span> h2 : 1 &gt; 0 := <span class="kw">by</span> <span class="kw">decide</span></span>
 <span id="cb57-22"><a href="#cb57-22" aria-hidden="true" tabindex="-1"></a>    <span class="kw">obtain</span> (x : U) (h3 : x ∈ A) <span class="kw">from</span> nonempty_of_pos_numElts h1 h2</span>
 <span id="cb57-23"><a href="#cb57-23" aria-hidden="true" tabindex="-1"></a>    <span class="kw">have</span> h4 : numElts (A \ {x}) 0 := remove_one_numElts h1 h3</span>
 <span id="cb57-24"><a href="#cb57-24" aria-hidden="true" tabindex="-1"></a>    <span class="kw">rewrite</span> [zero_elts_iff_empty] <span class="kw">at</span> h4</span>

lean.xml

@@ -62,6 +62,7 @@
 <item>ring</item>
 <item>linarith</item>
 <item>norm_num</item>
+<item>decide</item>
 <item>rel</item>
 <item>positivity</item>
 <item>trivial</item>