Commit Graph

12 Commits (main)

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 d519ef6b58 fix: adapt the rest of the program to the process refactor 2022-05-20 00:36:43 +02:00
Henrik Böving e0bf4ad28c doc: Output/Definition 2022-05-19 21:07:44 +02:00
Sebastian Ullrich 41f6eb0835 refactor: use `rawIdent` 2022-05-19 11:20:58 +02:00
Henrik Böving b87c1cc1de feat: Better equation Handling
The equation content is now escaped, furthermore there is a limit
for the length of an equation so we don't just fill everything with
uselessly big equations nobody can read anyways.
2022-02-20 13:45:18 +01:00
Xubai Wang 5e550c7833 refactor: docstring between basic and extra info
clean up code
2022-02-20 03:14:58 +08: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
Henrik Böving f54c192e6f feat: equations
Equation implementation for definitions, right now lots of definitions
simply dont generate equational lemmata at all so lots are left
without them.
2022-02-04 22:36:34 +01:00