Henrik Böving
|
64f627a295
|
chore: toolchain upgrade (#82)
Halleluja!
|
2022-10-05 12:05:58 +02:00 |
Sebastian Ullrich
|
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 |
|
Henrik Böving
|
23ddabb0da
|
Merge branch 'main' into LeanInkLink
|
2022-08-11 23:51:26 +02:00 |
|
Henrik Böving
|
cdfd8ff49c
|
feat: implement facet
|
2022-08-11 22:58:25 +02:00 |
|
Henrik Böving
|
6534a71cca
|
chore: update toolchain
|
2022-08-11 18:30:28 +02:00 |
|
Henrik Böving
|
d29e14a26a
|
chore: update toolchain and dependencies
|
2022-08-09 23:30:43 +02:00 |
|
Henrik Böving
|
763784e116
|
fix: whenever you force push a kitten dies
|
2022-07-26 15:17:56 +02:00 |
tydeu
|
5e78890ec0
|
feat: experimental module facet for producing docs
|
2022-07-23 21:18:35 -04:00 |
|
Henrik Böving
|
5f45c8dadc
|
chore: update toolchain
|
2022-07-20 16:29:18 +02:00 |
|
Henrik Böving
|
351cbc56b6
|
chore: update lean nightly
|
2022-07-04 09:11:10 +02:00 |
|
Henrik Böving
|
199c7af17a
|
feat: LeanInk all the files, HTML generation missing
|
2022-06-20 00:31:09 +02:00 |
|
Henrik Böving
|
0acf82bcbe
|
chore: update Unicode.lean
|
2022-06-19 17:03:26 +02:00 |
|
Henrik Böving
|
7c9237ffb4
|
chore: update compiler and lake
|
2022-06-19 16:41:59 +02:00 |
|
Henrik Böving
|
e8fb9a7f0f
|
chore: update to latest nightly
|
2022-05-27 22:19:34 +02:00 |
|
Henrik Böving
|
89dd2fa46e
|
chore: upgrade compiler version
|
2022-04-09 19:30:33 +02:00 |
|
Henrik Böving
|
9cc4c787e6
|
feat: lake integration
|
2022-03-06 18:51:06 +01:00 |
|
Henrik Böving
|
34d2239b68
|
feat: actual CLI
|
2022-02-23 22:54:10 +01:00 |
Xubai Wang
|
794923a997
|
fix: update Unicode.lean
|
2022-02-20 04:50:04 +08:00 |
|
Xubai Wang
|
5e550c7833
|
refactor: docstring between basic and extra info
clean up code
|
2022-02-20 03:14:58 +08:00 |
|
Xubai Wang
|
5679be6bbc
|
chore: bump lean version
update cmark version
|
2022-02-17 08:54:06 +08:00 |
|
Xubai Wang
|
8da2e2a63d
|
feat: basic docstring support
|
2022-02-17 08:16:02 +08:00 |
|
Henrik Böving
|
deb6739fcc
|
chore: Initial Lake project
|
2021-12-12 13:37:18 +01:00 |