Commit Graph

122 Commits (d8a5f52c101ac89c3445e028a5475752b64d52b6)

Author SHA1 Message Date
Xubai Wang d8a5f52c10 fix: fix docstring order 2022-02-18 11:28:44 +08:00
Xubai Wang 0724806fe6 Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring 2022-02-18 04:01:34 +08:00
Xubai Wang cce4285c96 fix: intersperse code contents 2022-02-18 04:01:31 +08:00
王虚白 5ce1ce9fe7
Merge branch 'main' into docstring 2022-02-18 03:38:20 +08:00
Xubai Wang 5dc3ab855f feat: config mathjax like doc-gen 2022-02-18 03:27:00 +08:00
Xubai Wang 9550d1c92e refactor: use ## for intra doc 2022-02-18 03:26:38 +08:00
Xubai Wang 89f5951f2d feat: add mathjax equation support 2022-02-18 03:10:48 +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 0b9a9f0bdc fix: remove intra link in code block 2022-02-18 01:39:02 +08:00
Xubai Wang 11bb2af57a feat: add auto link 2022-02-18 00:46:02 +08:00
Xubai Wang 97ddf05ab6 fix: add root to relative href 2022-02-17 21:26:02 +08:00
Xubai Wang 1729f4aa71 fix: fix docstring heading id 2022-02-17 15:26:17 +08:00
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 5679be6bbc chore: bump lean version
update cmark version
2022-02-17 08:54:06 +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 7d43c83178
Merge pull request #29 from leanprover/search
Search
2022-02-13 15:56:08 +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 96c8a048e3
Merge pull request #28 from leanprover/modifiers
Remaining modifiers for declarations
2022-02-13 03:35:21 +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 4490b1e674
Merge pull request #27 from leanprover/equations
Equations
2022-02-05 02:34:15 +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 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