Skip to content

Issues: leanprover/doc-gen4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

29 Open 54 Closed
29 Open 54 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

documentation no longer shows the list of all fields of a class/structure
#229 opened Nov 10, 2024 by alreadydone
1
too much space after Shrink.{u,v}
#226 opened Nov 1, 2024 by kbuzzard
1
Declarations not hyperlinked
#224 opened Oct 30, 2024 by fpvandoorn
class extends shows parents different from the code
#223 opened Oct 26, 2024 by alreadydone
1
Docs search ignores the exported name
#222 opened Oct 7, 2024 by YaelDillies
wrong links due to two definitions with same name
#219 opened Sep 28, 2024 by PhoenixIra
1
Clicking links in the navbar or using the "Go to source" link produces an error in VS Code webviews
#199 opened Jun 19, 2024 by mhuisi
noncomputable section isn't shown anywhere
#195 opened Jun 14, 2024 by Command-Master
2
auto-generated structure projections not appearing
#184 opened May 14, 2024 by fpvandoorn
2
Support for protected modifier
#180 opened Apr 12, 2024 by hargoniX
De-indent comment block
#165 opened Nov 23, 2023 by nomeata
3
Auto-generated lemmas appear before declaration
#163 opened Nov 14, 2023 by alreadydone
1
Show data fields only to avoid "not rendered due to size"
#160 opened Nov 12, 2023 by alreadydone
1
Improve UX for long instance names
#156 opened Oct 9, 2023 by utensil
1
Hyperlinking not working when an up-arrow occurs before the declaration name
#146 opened Sep 4, 2023 by BoltonBailey
Recover information about arguments of structures that we extend from
#139 opened Aug 22, 2023 by hargoniX
Generate hyperlinks for library note [XYZ] to the corresponding library_note doc-string.
#135 opened Aug 6, 2023 by kim-em
1
indexed DB invalidation
#133 opened Jul 20, 2023 by hargoniX
Show documentation for built-in Quot stuff good first issue Good for newcomers help wanted Extra attention is needed
#127 opened Apr 23, 2023 by hargoniX
Hyperlinking missing on some documentation
#104 opened Jan 1, 2023 by hrmacbeth
6
request: config file to set repo-specific information help wanted Extra attention is needed
#102 opened Dec 19, 2022 by hrmacbeth
1
request: in docs of a repository, display that repository differently from its dependencies
#101 opened Dec 19, 2022 by hrmacbeth
Input focus is stolen by left or right column help wanted Extra attention is needed
#94 opened Nov 21, 2022 by sgraf812
/find/ pages are recursive and broken
#92 opened Nov 19, 2022 by eric-wieser
10
Binder symbols in Exists is not linked
#91 opened Nov 19, 2022 by eric-wieser
2
ProTip! Add no:assignee to see everything that’s not assigned.