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

25 Open 58 Closed
25 Open 58 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

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
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
3
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
Hyperlinking not working when an up-arrow occurs before the declaration name
#146 opened Sep 4, 2023 by BoltonBailey
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
Linkify builtin types like Sort, Prop, and Pi
#90 opened Nov 14, 2022 by eric-wieser
1 of 3 tasks
3
Syntax declarations
#64 opened Jun 23, 2022 by hargoniX
@hargoniX
Populate the index page
#43 opened Feb 25, 2022 by xubaiw
Support unif_hint
#25 opened Jan 24, 2022 by hargoniX
ProTip! no:milestone will show everything without a milestone.