8059940c30
feat: class inductives
2022-02-06 20:14:36 +01:00
27f8b50763
feat: tag abbrevs
2022-02-06 17:28:56 +01:00
c2d18fe3b1
feat: tag declarations with unsafe and partial
2022-02-06 17:06:22 +01:00
5ef4ead859
Merge branch 'main' into equations
2022-02-05 02:31:00 +01:00
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
419c1eb1e6
feat: equations for instances
2022-02-04 22:48:08 +01:00
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
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
5ed0a8e99f
fix: do not show top-level modules twice in navbar
2022-01-20 15:38:48 +01:00
69b5ee76d3
chore: use attribute spreads
2022-01-20 15:38:48 +01:00
e350c16417
feat: `<div [attrArray] />`
2022-01-20 15:16:28 +01:00
9ac4eb5062
feat: imports, imported by
2022-01-16 14:22:53 +01:00
735bfa35a7
chore: update compiler version
2022-01-15 15:35:52 +01:00
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
f7f8138e09
feat: basic source links
2022-01-14 13:36:41 +01:00
0754b43873
feat: fix links to inductive ctors and structure fields
2022-01-09 14:07:50 +01:00
6128791cce
chore: Sort the declarations internally already
2022-01-07 18:25:26 +01:00
2de568d5ca
feat: List of declarations in internal navbar
2022-01-07 17:43:49 +01:00
82f63cb613
feat: parameterize the URL root for links in the HTML
2022-01-07 10:56:39 +01:00
ec4d114b43
feat: show all declarations in the correct order
...
Closes : #7
2022-01-06 17:30:33 +01:00
b777250338
feat: list instances of classes
2022-01-06 14:51:46 +01:00
87f959e11d
feat: basic structure like information for classes
2022-01-06 14:28:41 +01:00
f71b2ee8b9
chore: Remove obsolete TODOs
2022-01-06 02:05:23 +01:00
8a58752c56
feat: display structures and their fields properly
2022-01-06 01:44:11 +01:00
3adb8e71d1
feat: Show inductive constructors properly
...
Closes : #2
2022-01-03 18:22:12 +01:00
02d8c528d9
feat: Show arguments of types of decls separately
2022-01-03 14:25:55 +01:00
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
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
d18e71966c
feat: Store Format instead of Syntax in DocInfo
2021-12-18 00:01:31 +01:00
4380fe088d
feat: Sanitize Syntax
2021-12-17 23:53:06 +01:00
3c01cf1e68
feat: Name linking
2021-12-17 17:20:44 +01:00
ef716c9351
chore: Use builtin Name methods instead
2021-12-17 17:04:56 +01:00
2df4891c9f
feat: Setup infrastructure for type HTMLifying
2021-12-17 15:59:43 +01:00
03ec9c2e1d
chore: Cleanup the JSX parser a bit
2021-12-17 15:59:33 +01:00
dc5c2ab92a
chore: Add an HtmlT if we need more monads later on
2021-12-17 15:59:04 +01:00
cb582aab57
feat: Some more progress logging
2021-12-15 12:02:05 +01:00
b019faf7ba
feat: An initial list of declarations and their kinds
2021-12-15 11:59:36 +01:00
2adf5125c1
feat: Fix outputs paths
2021-12-15 11:59:13 +01:00
d5915fcb13
Revert "feat: Fix siteRoot in JS"
...
This reverts commit dcd57e8c5f
2021-12-15 11:25:10 +01:00
dcd57e8c5f
feat: Fix siteRoot in JS
2021-12-15 09:32:21 +01:00
686f111438
chore: Split Output.lean into multiple files
2021-12-15 09:24:49 +01:00
551eeee09d
feat: import nav.js
...
Just a copy and paste + include in the template, it will most likely
have to be modified in the future.
2021-12-13 21:36:21 +01:00
ef8ecec0d7
feat: Implement visibility in the navbar
2021-12-13 21:27:08 +01:00
d2594669fa
feat: Revamp the hierarchy mechanism
...
Previously the hierarchy mechanism wouldn't show modules in files that
have names, equal to some directory with submodules.
2021-12-13 20:47:52 +01:00
9256aaa0fc
feat: 404 page and module hierarchy
2021-12-13 13:00:53 +01:00
5e5bbe6ffb
chore: Update lean toolchain
2021-12-12 13:38:31 +01:00
dbbe11da0a
chore: In file licensing
2021-12-12 13:38:31 +01:00
ded884ce9c
feat: HTML Index + CSS
2021-12-12 13:38:31 +01:00
fcfe11e168
feat: Hierarchy datatype
2021-12-12 13:38:31 +01:00
0f0a355a93
feat: include_str macro for static file inclusion
2021-12-12 13:38:31 +01:00
0719fd6e30
feat: Allow Array Html as child of an HTMl node
2021-12-12 13:38:31 +01:00
413a24da56
feat: improve HTML to String a bit
2021-12-12 13:38:31 +01:00
c2da7afd76
chore: Update compiler and fix minor breaking change
2021-12-12 13:38:31 +01:00
e9a9e17439
feat: Basic Html to String converter
...
It works okay-ish for basic HTML which should be good enough for now
2021-12-12 13:38:31 +01:00
11de4f7f55
chore: Import ToHtmlFormat https://github.com/leanprover/lean4/pull/723
...
Added some slight modifications so it is inside the DocGen4 instead of
the Lean4.Widget namespace.
2021-12-12 13:38:31 +01:00
77cb52e9cb
chore: Inline licensing
2021-12-12 13:38:31 +01:00
7785c9f5bd
feat: Fetch declaration ranges for constants
2021-12-12 13:38:31 +01:00
29a249e8fd
feat: Automatic search path + modules as CLI arguments
2021-12-12 13:38:27 +01:00
4d8aa10ecb
chore: Little refactoring for Name x Syntax tuples
2021-12-12 13:38:24 +01:00
821d57fd1c
feat: Also print parents in structures and classes
2021-12-12 13:38:19 +01:00
b60eca730f
chore: Fill universe MVars and remove out of date TODOs
2021-12-12 13:38:11 +01:00
82c78d29bd
feat: rudimentary structure field support
2021-12-12 13:38:07 +01:00
b8cf967b84
chore: Focus on basic declarations for now
2021-12-12 13:38:02 +01:00
ac8d9e254e
feat: parenthesize in the pretty printer
2021-12-12 13:37:59 +01:00
8c30f29542
feat: Instance support
2021-12-12 13:37:56 +01:00
a6979dd3d4
feat: Rudamentary class support
2021-12-12 13:37:53 +01:00
989e7bce2b
feat: Filter projection functions from defs
2021-12-12 13:37:49 +01:00
006b92deaa
feat: Rudamentary structure support
2021-12-12 13:37:46 +01:00
21bcc3d0bc
feat: Print definitions and inductives
2021-12-12 13:37:42 +01:00
d2fddd7cff
feat: Print count of declarations and modules processed
2021-12-12 13:37:38 +01:00
dd0cebb44a
feat: Sort everything into modules instead of just declaration lists
2021-12-12 13:37:28 +01:00
2574c22e4a
feat: First experimentations
2021-12-12 13:37:25 +01:00
Henrik Böving
Gabriel Ebner