3687b3466a
refactor: clean up docstring module
2022-02-18 12:52:01 +08:00
5ce1ce9fe7
Merge branch 'main' into docstring
2022-02-18 03:38:20 +08:00
2dac93d360
fix: fix noncomputable
...
Also address the changes made to module doc until doc strings are implemented.
2022-02-17 18:59:42 +01:00
385a38a003
feat: basic mod doc without attributes
2022-02-17 08:16:02 +08:00
e6cc03b095
fix: Fix computability
2022-02-13 15:52:09 +01:00
c42db4328a
feat: export search.js info
2022-02-13 15:03:49 +01:00
d700da7284
feat: Attributes
2022-02-13 03:32:53 +01:00
59e50943d6
feat: mark noncomputable defs and instances
2022-02-12 15:57:45 +01:00
d39b14cf7a
chore: bump toolchain, bye auto pure
2022-02-12 15:09:13 +01:00
00bf10c6f0
chore: bump toolchain
2022-02-09 22:45:28 +01:00
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
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
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
9ac4eb5062
feat: imports, imported by
2022-01-16 14:22:53 +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
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
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
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
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
2df4891c9f
feat: Setup infrastructure for type HTMLifying
2021-12-17 15:59:43 +01:00
b019faf7ba
feat: An initial list of declarations and their kinds
2021-12-15 11:59:36 +01:00
ded884ce9c
feat: HTML Index + CSS
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
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
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
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
Xubai Wang
王虚白
Henrik Böving