Henrik Böving 2e4642e17c chore: port legacy syntax to rawIdent		2022-05-19 17:16:40 +02:00
..
Base.lean	chore: upgrade compiler version	2022-04-09 19:30:33 +02:00
Class.lean	refactor: docstring between basic and extra info	2022-02-20 03:14:58 +08:00
ClassInductive.lean	refactor: docstring between basic and extra info	2022-02-20 03:14:58 +08:00
Definition.lean	refactor: use `rawIdent`	2022-05-19 11:20:58 +02:00
DocString.lean	chore: upgrade compiler version	2022-04-09 19:30:33 +02:00
Find.lean	fix: port the SITE_ROOT fix to find.js	2022-04-07 13:14:01 +02:00
Index.lean	chore: bump toolchain, bye auto pure	2022-02-12 15:09:13 +01:00
Inductive.lean	chore: port legacy syntax to rawIdent	2022-05-19 17:16:40 +02:00
Instance.lean	refactor: docstring between basic and extra info	2022-02-20 03:14:58 +08:00
Module.lean	refactor: use `rawIdent`	2022-05-19 11:20:58 +02:00
Navbar.lean	chore: port legacy syntax to rawIdent	2022-05-19 17:16:40 +02:00
NotFound.lean	chore: bump toolchain, bye auto pure	2022-02-12 15:09:13 +01:00
Semantic.lean	refactor: change find syntax	2022-02-23 04:26:20 +08:00
Structure.lean	refactor: use `rawIdent`	2022-05-19 11:20:58 +02:00
Template.lean	refactor: use `rawIdent`	2022-05-19 11:20:58 +02:00