Commit Graph

17 Commits (9220cd74b136e3283cc7ced0d6e145e7b8800fe1)

Author SHA1 Message Date
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