Commit Graph

10 Commits (e888e9cc383f838ef8f519e6941e32fe5c48df1b)

Author SHA1 Message Date
Jeremy Salwen 033003c6cb Add a search page to the docs.
Now instead of clicking the "Google Site Search"' button, the user has the option
of clicking the "Search" button, which will take them to a results page. Currently,
the results are identical to the autocomplete results, but the number of results
is not limited to 30.  In the future, more information and search options could
be added to this page to make a more powerful search.

Fixes #107
2023-01-28 23:00:53 +01:00
Henrik Böving 3a5c0db46b style: refactor process to Lean 4 compiler style 2023-01-01 19:30:28 +01:00
Henrik Böving 72034b0831 feat: linkify builtin types 2022-11-22 21:07:59 +01:00
Mario Carneiro 9aef28b16e
chore: update toolchain 10-20 (#86) 2022-10-20 19:51:26 +02:00
Henrik Böving 64f627a295
chore: toolchain upgrade (#82)
Halleluja!
2022-10-05 12:05:58 +02:00
tydeu 2cc851aaf1 fix: include top-level modules in hierarchy and exclude non-html 2022-07-23 22:02:20 -04:00
Henrik Böving ed4cee2eae chore: style, change $ to <| 2022-07-23 13:01:25 +02:00
Henrik Böving c29cf7b70c feat: index shall not depend on importing things 2022-07-22 00:34:13 +02:00
Henrik Böving 25b1ddb66b feat: Preparations to split doc-gen build process 2022-07-21 01:40:04 +02:00
Henrik Böving 279df92555 refactor: restructure the modules 2022-05-19 20:41:07 +02:00