Henrik Böving
|
3cc5df1be7
|
feat: fix #166
|
2023-11-24 13:45:47 +01:00 |
Eric Wieser
|
d3d67c1d92
|
Do the same for inductives
|
2023-08-18 11:00:32 +02:00 |
|
Henrik Böving
|
f74443a673
|
style: Lean 4 compiler style in output
|
2023-01-01 19:51:01 +01:00 |
|
Henrik Böving
|
b22818b971
|
feat: render foundational types info
|
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
|
247b930364
|
feat: instances for
|
2022-07-23 15:40:08 +02:00 |
|
Henrik Böving
|
601b895e89
|
feat: Inductive constructor doc strings
|
2022-07-21 20:23:27 +02:00 |
|
Henrik Böving
|
d519ef6b58
|
fix: adapt the rest of the program to the process refactor
|
2022-05-20 00:36:43 +02:00 |
|
Henrik Böving
|
2e4642e17c
|
chore: port legacy syntax to rawIdent
|
2022-05-19 17:16:40 +02:00 |
Sebastian Ullrich
|
41f6eb0835
|
refactor: use `rawIdent`
|
2022-05-19 11:20:58 +02:00 |
Xubai Wang
|
d8a5f52c10
|
fix: fix docstring order
|
2022-02-18 11:28:44 +08:00 |
|
Xubai Wang
|
97ddf05ab6
|
fix: add root to relative href
|
2022-02-17 21:26:02 +08:00 |
|
Xubai Wang
|
b7c6a98969
|
refactor: separate docstring code
|
2022-02-17 13:47:38 +08:00 |
|
Xubai Wang
|
8da2e2a63d
|
feat: basic docstring support
|
2022-02-17 08:16:02 +08:00 |
|
Henrik Böving
|
d39b14cf7a
|
chore: bump toolchain, bye auto pure
|
2022-02-12 15:09:13 +01:00 |
Gabriel Ebner
|
69b5ee76d3
|
chore: use attribute spreads
|
2022-01-20 15:38:48 +01:00 |
|
Henrik Böving
|
0754b43873
|
feat: fix links to inductive ctors and structure fields
|
2022-01-09 14:07:50 +01:00 |
|
Henrik Böving
|
8a58752c56
|
feat: display structures and their fields properly
|
2022-01-06 01:44:11 +01:00 |
|
Henrik Böving
|
3adb8e71d1
|
feat: Show inductive constructors properly
Closes: #2
|
2022-01-03 18:22:12 +01:00 |