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
2e62f636f4
Merge pull request #26 from leanprover/custom-ctors
...
feat: Custom structure ctors
2022-02-02 12:56:30 +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
Henrik Böving
b1abc677a0
Merge pull request #24 from gebner/navbarheaders
...
fix: do not show top-level modules twice in navbar
2022-01-20 20:18:41 +01:00
Gabriel Ebner
fd5280f30a
fix: print usage when called without arguments
2022-01-20 15:38:48 +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
0be10cfad6
Merge pull request #21 from leanprover/imports
...
imports, imported by
2022-01-16 14:29:13 +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
1edf4bbdab
Merge pull request #20 from leanprover/fix-anonymous-arrows
...
fix: Printing of argument names with macro scopes
2022-01-15 15:17:44 +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
b93e1c9f54
Merge pull request #19 from leanprover/source-links
...
Basic source links
2022-01-14 13:38:58 +01:00
Henrik Böving
f7f8138e09
feat: basic source links
2022-01-14 13:36:41 +01:00
Henrik Böving
0751cea667
Merge pull request #18 from leanprover/constructor-links
...
Fix links to inductive constructors and structure fields
2022-01-09 14:10:25 +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
b90644cfd2
Merge pull request #17 from leanprover/sidebar-names
...
Sidebar names
2022-01-07 18:29:01 +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
49fdb6279d
chore: Switch to leanprover community bot email for automated doc updates
2022-01-07 10:44:11 +01:00
Henrik Böving
08c1770655
Merge pull request #16 from leanprover/cicd
...
CI and auto documentation preview for mathlib4
2022-01-07 10:37:32 +01:00
Henrik Böving
93f32971ec
feat: CI and auto documentation preview for mathlib4
2022-01-07 10:29:15 +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
eae71c61a3
Merge pull request #14 from leanprover/class
...
Typeclass and instances handling
2022-01-06 14:52:21 +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
e67ea1d1f0
feat: change CSS to acount for classes and instances
2022-01-06 14:19:14 +01:00
Henrik Böving
598e5835e7
Merge pull request #13 from leanprover/structure
...
Structure support
2022-01-06 02:06:10 +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
3f1c0ecd77
chore: Update lean-toolchain
2022-01-04 08:24:59 +01:00
Henrik Böving
3adb8e71d1
feat: Show inductive constructors properly
...
Closes : #2
2022-01-03 18:22:12 +01:00
Henrik Böving
85d1e4608c
Merge pull request #1 from hargoniX/main
...
Initial implementation
2022-01-03 14:29:58 +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
Henrik Böving
b019faf7ba
feat: An initial list of declarations and their kinds
2021-12-15 11:59:36 +01:00