Update blurb

blurb.html

@@ -31,30 +31,37 @@ <h2 id="documentation">Documentation</h2>
 <li><p>By subexpression:</p>
 <pre class="lean"><code>#find _ * (_ ^ _)</code></pre>
 <p>finds all lemmas whose statements somewhere include a product where
-the second argument is raised to some power. The pattern can also be
-non-linear, as in</p>
-<pre class="lean"><code>#find Real.sqrt ?a * Real.sqrt ?a</code></pre></li>
-<li><p>By conclusion and/or hypothesis:</p>
+the second argument is raised to some power.</p>
+<p>The pattern can also be non-linear, as in</p>
+<pre class="lean"><code>#find Real.sqrt ?a * Real.sqrt ?a</code></pre>
+<p>If the pattern has parameters, they are matched in any order. Both of
+these will find <code>List.map</code>:</p>
+<pre><code>#find (?a -&gt; ?b) -&gt; List ?a -&gt; List ?b
+#find List ?a -&gt; (?a -&gt; ?b) -&gt; List ?b</code></pre></li>
+<li><p>By main conclusion:</p>
 <pre class="lean"><code>#find ⊢ tsum _ = _ * tsum _</code></pre>
 <p>finds all lemmas where the conclusion (the subexpression to the right
-of all <code>→</code> and <code>∀</code>) has the given shape. If the
-pattern has hypotheses, they are matched against the hypotheses of the
-lemma in any order; for example,</p>
+of all <code>→</code> and <code>∀</code>) has the given shape.</p>
+<p>As before, if the pattern has parameters, they are matched against
+the hypotheses of the lemma in any order; for example,</p>
 <pre class="lean"><code>#find ⊢ _ &lt; _ → tsum _ &lt; tsum _</code></pre>
 <p>will find <code>tsum_lt_tsum</code> even though the hypothesis
 <code>f i &lt; g i</code> is not the last.</p></li>
-<li><p>In combination:</p>
+</ol>
+<p>If you pass more than one such search filter, <code>#find</code> will
+return lemmas which match <em>all</em> of them. The search</p>
 <pre class="lean"><code>#find Real.sin, &quot;two&quot;, tsum,  _ * _, _ ^ _, ⊢ _ &lt; _ → _</code></pre>
 <p>will find all lemmas which mention the constants
 <code>Real.sin</code> and <code>tsum</code>, have <code>"two"</code> as
 a substring of the lemma name, include a product and a power somewhere
 in the type, <em>and</em> have a hypothesis of the form
-<code>_ &lt; _</code>.</p></li>
-</ol>
-<p>If you pass more than one such search filter, <code>#find</code> will
-only return lemmas which match <em>all</em> of them simultaneously. At
-least some filter must mention a concrete name, because
-<code>#find</code> maintains</p>
+<code>_ &lt; _</code>.</p>
+<p>At least some filter must mention a concrete name, because
+<code>#find</code> maintains an index of which lemmas mention which
+other constants. This is also why the <em>first</em> use of
+<code>#find</code> will be somewhat slow (typically less than half a
+minute with all of <code>Mathlib</code> imported), but subsequent uses
+are faster.</p>
 <h2 id="source-code">Source code</h2>
 <p>You can find the source code for this service at <a
 href="https://github.com/nomeata/loogle"

blurb.md

@@ -34,33 +34,47 @@ combined in a single query, comma-separated.
    #find _ * (_ ^ _)
    ```
    finds all lemmas whose statements somewhere include a product where the second argument is
-   raised to some power. The pattern can also be non-linear, as in
+   raised to some power.
+
+   The pattern can also be non-linear, as in
    ```lean
    #find Real.sqrt ?a * Real.sqrt ?a
    ```
 
-4. By conclusion and/or hypothesis:
+   If the pattern has parameters, they are matched in any order. Both of these will find `List.map`:
+   ```
+   #find (?a -> ?b) -> List ?a -> List ?b
+   #find List ?a -> (?a -> ?b) -> List ?b
+   ```
+
+4. By main conclusion:
    ```lean
    #find ⊢ tsum _ = _ * tsum _
    ```
    finds all lemmas where the conclusion (the subexpression to the right of all `→` and `∀`) has the
-   given shape. If the pattern has hypotheses, they are matched against the hypotheses of
+   given shape.
+
+   As before, if the pattern has parameters, they are matched against the hypotheses of
    the lemma in any order; for example,
    ```lean
    #find ⊢ _ < _ → tsum _ < tsum _
    ```
    will find `tsum_lt_tsum` even though the hypothesis `f i < g i` is not the last.
 
-5. In combination:
-   ```lean
-   #find Real.sin, "two", tsum,  _ * _, _ ^ _, ⊢ _ < _ → _
-   ```
-   will find all lemmas which mention the constants `Real.sin` and `tsum`, have `"two"` as a
-   substring of the lemma name, include a product and a power somewhere in the type, *and* have a
-   hypothesis of the form `_ < _`.
 
-If you pass more than one such search filter, `#find` will only return lemmas which match _all_ of
-them simultaneously. At least some filter must mention a concrete name, because `#find` maintains
+If you pass more than one such search filter, `#find` will return lemmas which match _all_ of them.
+The search
+```lean
+#find Real.sin, "two", tsum,  _ * _, _ ^ _, ⊢ _ < _ → _
+```
+will find all lemmas which mention the constants `Real.sin` and `tsum`, have `"two"` as a
+substring of the lemma name, include a product and a power somewhere in the type, *and* have a
+hypothesis of the form `_ < _`.
+
+At least some filter must mention a concrete name, because `#find` maintains an index of which
+lemmas mention which other constants. This is also why the _first_ use of `#find` will be somewhat
+slow (typically less than half a minute with all of `Mathlib` imported), but subsequent uses are
+faster.
 
 ## Source code