e5b44f1cdf
chore: update toolchain
2023-04-16 01:30:21 +02:00
5ab7d0bdd8
fix: unicode dependency
2023-03-15 11:54:57 +01:00
5f59fbaac4
refactor: switch to maintained unicode lib
2023-03-11 18:06:32 +01:00
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
7009910876
chore: update toolchain
2022-12-03 17:43:12 +01:00
9aef28b16e
chore: update toolchain 10-20 ( #86 )
2022-10-20 19:51:26 +02:00
64f627a295
chore: toolchain upgrade ( #82 )
...
Halleluja!
2022-10-05 12:05:58 +02:00
4a7c5e214a
chore: drop unused import
...
I didn't even know one could import modules from executables! Not sure how to feel about that.
2022-08-12 23:04:36 +02:00
23ddabb0da
Merge branch 'main' into LeanInkLink
2022-08-11 23:51:26 +02:00
cdfd8ff49c
feat: implement facet
2022-08-11 22:58:25 +02:00
6534a71cca
chore: update toolchain
2022-08-11 18:30:28 +02:00
d29e14a26a
chore: update toolchain and dependencies
2022-08-09 23:30:43 +02:00
763784e116
fix: whenever you force push a kitten dies
2022-07-26 15:17:56 +02:00
5e78890ec0
feat: experimental module facet for producing docs
2022-07-23 21:18:35 -04:00
5f45c8dadc
chore: update toolchain
2022-07-20 16:29:18 +02:00
351cbc56b6
chore: update lean nightly
2022-07-04 09:11:10 +02:00
199c7af17a
feat: LeanInk all the files, HTML generation missing
2022-06-20 00:31:09 +02:00
0acf82bcbe
chore: update Unicode.lean
2022-06-19 17:03:26 +02:00
7c9237ffb4
chore: update compiler and lake
2022-06-19 16:41:59 +02:00
e8fb9a7f0f
chore: update to latest nightly
2022-05-27 22:19:34 +02:00
89dd2fa46e
chore: upgrade compiler version
2022-04-09 19:30:33 +02:00
9cc4c787e6
feat: lake integration
2022-03-06 18:51:06 +01:00
34d2239b68
feat: actual CLI
2022-02-23 22:54:10 +01:00
794923a997
fix: update Unicode.lean
2022-02-20 04:50:04 +08:00
5e550c7833
refactor: docstring between basic and extra info
...
clean up code
2022-02-20 03:14:58 +08:00
5679be6bbc
chore: bump lean version
...
update cmark version
2022-02-17 08:54:06 +08:00
8da2e2a63d
feat: basic docstring support
2022-02-17 08:16:02 +08:00
deb6739fcc
chore: Initial Lake project
2021-12-12 13:37:18 +01:00
Henrik Böving
F. G. Dorais
Jeremy Salwen
Mario Carneiro
Sebastian Ullrich
tydeu
Xubai Wang