Commit Graph

102 Commits (e6cc03b095831a352d94546edb0a6e2a70488574)

Author SHA1 Message Date
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
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