Henrik Böving
211ade7828
feat: doc strings in ctors and structure fields
2022-04-09 17:27:06 +02:00
Xubai Wang
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
Henrik Böving
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
Xubai Wang
385a38a003
feat: basic mod doc without attributes
2022-02-17 08:16:02 +08:00
Henrik Böving
e6cc03b095
fix: Fix computability
2022-02-13 15:52:09 +01:00
Henrik Böving
c42db4328a
feat: export search.js info
2022-02-13 15:03:49 +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
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
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
9ac4eb5062
feat: imports, imported by
2022-01-16 14:22:53 +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
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
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
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
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
2df4891c9f
feat: Setup infrastructure for type HTMLifying
2021-12-17 15:59:43 +01:00
Henrik Böving
b019faf7ba
feat: An initial list of declarations and their kinds
2021-12-15 11:59:36 +01:00
Henrik Böving
ded884ce9c
feat: HTML Index + CSS
2021-12-12 13:38:31 +01:00
Henrik Böving
c2da7afd76
chore: Update compiler and fix minor breaking change
2021-12-12 13:38:31 +01:00
Henrik Böving
77cb52e9cb
chore: Inline licensing
2021-12-12 13:38:31 +01:00
Henrik Böving
7785c9f5bd
feat: Fetch declaration ranges for constants
2021-12-12 13:38:31 +01:00
Henrik Böving
4d8aa10ecb
chore: Little refactoring for Name x Syntax tuples
2021-12-12 13:38:24 +01:00
Henrik Böving
821d57fd1c
feat: Also print parents in structures and classes
2021-12-12 13:38:19 +01:00
Henrik Böving
b60eca730f
chore: Fill universe MVars and remove out of date TODOs
2021-12-12 13:38:11 +01:00
Henrik Böving
82c78d29bd
feat: rudimentary structure field support
2021-12-12 13:38:07 +01:00
Henrik Böving
b8cf967b84
chore: Focus on basic declarations for now
2021-12-12 13:38:02 +01:00
Henrik Böving
ac8d9e254e
feat: parenthesize in the pretty printer
2021-12-12 13:37:59 +01:00
Henrik Böving
8c30f29542
feat: Instance support
2021-12-12 13:37:56 +01:00
Henrik Böving
a6979dd3d4
feat: Rudamentary class support
2021-12-12 13:37:53 +01:00
Henrik Böving
989e7bce2b
feat: Filter projection functions from defs
2021-12-12 13:37:49 +01:00
Henrik Böving
006b92deaa
feat: Rudamentary structure support
2021-12-12 13:37:46 +01:00
Henrik Böving
21bcc3d0bc
feat: Print definitions and inductives
2021-12-12 13:37:42 +01:00
Henrik Böving
dd0cebb44a
feat: Sort everything into modules instead of just declaration lists
2021-12-12 13:37:28 +01:00
Henrik Böving
2574c22e4a
feat: First experimentations
2021-12-12 13:37:25 +01:00