diff --git a/vscode-lean4/loogleview/static/index.html b/vscode-lean4/loogleview/static/index.html index 6fc431c1..c58cb7eb 100644 --- a/vscode-lean4/loogleview/static/index.html +++ b/vscode-lean4/loogleview/static/index.html @@ -27,52 +27,64 @@

Usage

  1. - By constant:
    - Real.sin finds all lemmas whose statement somehow mentions the sinefunction. + By constant:
    + Real.sin finds all lemmas whose statement somehow + mentions the sinefunction.

  2. - By lemma name substring:
    - "differ" finds all lemmas that have "differ" somewhere in their lemma name. + By lemma name substring:
    + "differ" finds all lemmas that have + "differ" somewhere in their lemma name.

  3. - By subexpression:
    - _ * (_ ^ _) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power. + By subexpression:
    + _ * (_ ^ _) 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 Real.sqrt ?a * Real.sqrt ?a + The pattern can also be non-linear, as in + Real.sqrt ?a * Real.sqrt ?a

    - If the pattern has parameters, they are matched in any order. Both of these will find List.map:
    - (?a -> ?b) -> List ?a -> List ?b
    + If the pattern has parameters, they are matched in any order. Both of these will find + List.map:
    + (?a -> ?b) -> List ?a -> List ?b
    List ?a -> (?a -> ?b) -> List ?b

  4. - By main conclusion:
    - |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape. + By main conclusion:
    + |- tsum _ = _ * tsum _ finds all lemmas where the + conclusion (the subexpression to the right of all → and ∀) has the given shape.

    - As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last. + As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; + for example, |- _ < _ → tsum _ < tsum _ will + find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

- If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ - would 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 - there were any such lemmas). Metavariables (?a) are - assigned independently in each filter. + If you pass more than one such search filter, separated by commas Loogle will return lemmas which match + all of them. The search + Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ would + 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 there were any such lemmas). Metavariables (?a) are assigned + independently in each filter.

Source code

-

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is currently -provided by Joachim Breitner <mail@joachim-breitner.de>.

+

+ You can find the source code for this service at + https://github.com/nomeata/loogle. The + https://loogle.lean-lang.org/ service is currently provided + by Joachim Breitner <mail@joachim-breitner.de>. +