Commit Graph

86 Commits (5790172eab2a45bb4c98fbf463c7d175876b588c)

Author SHA1 Message Date
Xubai Wang 5790172eab fix: doc string for all DocInfo 2022-02-17 13:53:29 +08:00
Xubai Wang b7c6a98969 refactor: separate docstring code 2022-02-17 13:47:38 +08:00
Xubai Wang d3ce268d63 feat: mod doc heading attributes 2022-02-17 08:16:02 +08:00
Xubai Wang 385a38a003 feat: basic mod doc without attributes 2022-02-17 08:16:02 +08:00
Xubai Wang 8da2e2a63d feat: basic docstring support 2022-02-17 08:16:02 +08:00
Henrik Böving 28dfc14530 fix: arity in the extern attribute 2022-02-16 21:24:42 +01:00
Henrik Böving e6cc03b095 fix: Fix computability 2022-02-13 15:52:09 +01:00
Henrik Böving 5fd2585c55 feat: Implement the rest of search 2022-02-13 15:42:15 +01:00
Henrik Böving c42db4328a feat: export search.js info 2022-02-13 15:03:49 +01:00
Henrik Böving 4b9b7d77d5 chore: Update doc-gen search js 2022-02-13 14:25:37 +01:00
Henrik Böving d700da7284 feat: Attributes 2022-02-13 03:32:53 +01:00
Henrik Böving 59e50943d6 feat: mark noncomputable defs and instances 2022-02-12 15:57:45 +01:00
Henrik Böving d39b14cf7a chore: bump toolchain, bye auto pure 2022-02-12 15:09:13 +01:00
Henrik Böving 00bf10c6f0 chore: bump toolchain 2022-02-09 22:45:28 +01:00
Henrik Böving 8059940c30 feat: class inductives 2022-02-06 20:14:36 +01:00
Henrik Böving 27f8b50763 feat: tag abbrevs 2022-02-06 17:28:56 +01:00
Henrik Böving c2d18fe3b1 feat: tag declarations with unsafe and partial 2022-02-06 17:06:22 +01:00
Henrik Böving 5ef4ead859
Merge branch 'main' into equations 2022-02-05 02:31:00 +01:00
Henrik Böving 117c94031f feat: equations for simple functions
Functions without pattern matching or wf recursion don't have
any equational lemma autogenerated for themselves so we have to
generate it explicitly. The implementation is largely adapted from
structural equation code in the compiler.
2022-02-05 02:26:03 +01:00
Henrik Böving 419c1eb1e6 feat: equations for instances 2022-02-04 22:48:08 +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
Henrik Böving 4d63f90449 feat: Custom structure ctors
Add the ability to show customly named structure constructors as well
as a little cosmetic change to how structure fields are displayed.
2022-02-02 12:53:04 +01:00
Gabriel Ebner 5ed0a8e99f fix: do not show top-level modules twice in navbar 2022-01-20 15:38:48 +01:00
Gabriel Ebner 69b5ee76d3 chore: use attribute spreads 2022-01-20 15:38:48 +01:00
Gabriel Ebner e350c16417 feat: `<div [attrArray] />` 2022-01-20 15:16:28 +01:00
Henrik Böving 9ac4eb5062 feat: imports, imported by 2022-01-16 14:22:53 +01:00
Henrik Böving 735bfa35a7 chore: update compiler version 2022-01-15 15:35:52 +01:00
Henrik Böving 4a3e22490f fix: Printing of argument names with macro scopes
Previously we would print all names with macro scopes (after removing
the macro related stuff) which could cause confusion if for example
there was an actual parameter named `a` and one named `a` but
autogenerated by Lean itself. Now we only try to print names with
macro scopes iff they are names of type class parameters. Otherwise
the rest of the Expr is moved behind the :.
2022-01-15 15:12:55 +01:00
Henrik Böving f7f8138e09 feat: basic source links 2022-01-14 13:36:41 +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 6128791cce chore: Sort the declarations internally already 2022-01-07 18:25:26 +01:00
Henrik Böving 2de568d5ca feat: List of declarations in internal navbar 2022-01-07 17:43:49 +01:00
Henrik Böving 82f63cb613 feat: parameterize the URL root for links in the HTML 2022-01-07 10:56:39 +01:00
Henrik Böving ec4d114b43 feat: show all declarations in the correct order
Closes: #7
2022-01-06 17:30:33 +01:00
Henrik Böving b777250338 feat: list instances of classes 2022-01-06 14:51:46 +01:00
Henrik Böving 87f959e11d feat: basic structure like information for classes 2022-01-06 14:28:41 +01:00
Henrik Böving f71b2ee8b9 chore: Remove obsolete TODOs 2022-01-06 02:05:23 +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
Henrik Böving 02d8c528d9 feat: Show arguments of types of decls separately 2022-01-03 14:25:55 +01:00
Henrik Böving 5e0956c4b0 feat: Proper linking of all constants
Previously constants in function applications where either not linked
at all or linked in a weird way, this change fixes it by making use of
a (as of now umerged) compiler modification as well as Lean.Widget's
TaggedText.
2022-01-03 14:25:50 +01:00
Henrik Böving 0efbcd1f60 feat: Newline free HTML formatting
Some of the HTML elements we are generating are newline sensitive
which requires the HTML to String formatter to optionally omit
additional newlines.
2021-12-25 14:04:35 +01:00
Henrik Böving d18e71966c feat: Store Format instead of Syntax in DocInfo 2021-12-18 00:01:31 +01:00
Henrik Böving 4380fe088d feat: Sanitize Syntax 2021-12-17 23:53:06 +01:00
Henrik Böving 3c01cf1e68 feat: Name linking 2021-12-17 17:20:44 +01:00
Henrik Böving ef716c9351 chore: Use builtin Name methods instead 2021-12-17 17:04:56 +01:00
Henrik Böving 2df4891c9f feat: Setup infrastructure for type HTMLifying 2021-12-17 15:59:43 +01:00
Henrik Böving 03ec9c2e1d chore: Cleanup the JSX parser a bit 2021-12-17 15:59:33 +01:00
Henrik Böving dc5c2ab92a chore: Add an HtmlT if we need more monads later on 2021-12-17 15:59:04 +01:00
Henrik Böving cb582aab57 feat: Some more progress logging 2021-12-15 12:02:05 +01:00