leanprover/doc-gen4

Issues

• Implement references / bibliography

  #147 opened 6 months ago by alexjbest
  7

• Hyperlinking missing on some documentation

  #104 opened 2 years ago by hrmacbeth
  6

• Clicking links in the navbar or using the "Go to source" link produces an error in VS Code webviews

  #199 opened 6 months ago by mhuisi
  0

• noncomputable section isn't shown anywhere

  #195 opened 7 months ago by Command-Master
  2

• Escape sequences are handled incorrectly in LaTeX

  #178 opened 7 months ago by eric-wieser
  9

• De-indent comment block

  #165 opened a year ago by nomeata
  3

• /find/ pages are recursive and broken

  #92 opened 2 years ago by eric-wieser
  10

• Mangled docstring for `congrArg`

  #126 opened 7 months ago by chabulhwi
  2

• auto-generated structure projections not appearing

  #184 opened 8 months ago by fpvandoorn
  2

• Support for protected modifier

  #180 opened 9 months ago by hargoniX
  0

• Empty instances for

  #166 opened a year ago by nomeata
  1

• important type info is omitted

  #140 opened a year ago by alreadydone
  3

• Linkify builtin types like `Sort`, `Prop`, and `Pi`

  #90 opened 2 years ago by eric-wieser
  3

• doc-gen: Explorability of theories

  #77 opened a year ago by hargoniX
  1

• Auto-generated lemmas appear before declaration

  #163 opened a year ago by alreadydone
  1

• Put inductive/structure documentation before field documentation

  #161 opened a year ago by nomeata
  3

• Show data fields only to avoid "not rendered due to size"

  #160 opened a year ago by alreadydone
  1

• instances for vs instances mentioning

  #158 opened a year ago by hargoniX
  0

• Truncated docs page?

  #136 opened a year ago by alreadydone
  2

• Improve UX for long instance names

  #156 opened a year ago by utensil
  1

• Lean statement not rendered for theorems defined as `def thm : Prop := statement`

  #155 opened a year ago by utensil
  0

• Unclear error when running in a git repo without "origin" remote

  #150 opened a year ago by Ruben-VandeVelde
  1

• request: have the path to the current position unfolded by default

  #106 opened a year ago by hrmacbeth
  1

• Consider refactoring the navbar

  #69 opened a year ago by hargoniX
  1

• Hyperlinking not working when an up-arrow occurs before the declaration name

  #146 opened a year ago by BoltonBailey
  0

• @[reducible] attributes are not shown

  #144 opened a year ago by alreadydone
  1

• ERROR: could not execute external process 'cc'

  #143 opened a year ago by Seasawher
  2

• error: no such file or directory

  #142 opened a year ago by Seasawher
  4

• Recover information about arguments of structures that we extend from

  #139 opened a year ago by hargoniX
  0

• Generate hyperlinks for `library note [XYZ]` to the corresponding `library_note` doc-string.

  #135 opened a year ago by kim-em
  1

• indexed DB invalidation

  #133 opened a year ago by hargoniX
  0

• Support prefers-color-scheme media query

  #117 opened 2 years ago by 4e554c4c
  1

• Show documentation for built-in Quot stuff

  #127 opened 2 years ago by hargoniX
  0

• Mangled docstring for `CoeHTCT`

  #123 opened 2 years ago by eric-wieser
  2

• request: in the right sidebar, prioritize linebreaks at `.`

  #100 opened 2 years ago by hrmacbeth
  2

• Lines don't wrap in the instance list of some declarations

  #105 opened 2 years ago by hrmacbeth
  1

• Linkifier to fields and constructors

  #113 opened 2 years ago by fpvandoorn
  0

• Linkifier to special characters

  #114 opened 2 years ago by fpvandoorn
  1

• Show full results for search

  #107 opened 2 years ago by jeremysalwen
  10

• request: config file to set repo-specific information

  #102 opened 2 years ago by hrmacbeth
  1

• Input focus is stolen by left or right column

  #94 opened 2 years ago by sgraf812
  0

• request: for a file + folder with same name, give more screen real estate to the folder

  #99 opened 2 years ago by hrmacbeth
  5

• request: in docs of a repository, display that repository differently from its dependencies

  #101 opened 2 years ago by hrmacbeth
  0

• Request: In library directory sidebar, do not repeat the full address of files

  #95 opened 2 years ago by hrmacbeth
  3

• Request: In library directory sidebar, preserve folded/unfolded state of each directory after a click

  #96 opened 2 years ago by hrmacbeth
  1

• Binder symbols in Exists is not linked

  #91 opened 2 years ago by eric-wieser
  2

• Missing space between declaration name without parameters and `:`

  #76 opened 2 years ago by Kha
  0

• Discoverability of typeclass instances

  #63 opened 2 years ago by hargoniX
  0

• Syntax declarations

  #64 opened 3 years ago by hargoniX
  0

• Docstrings on inductives

  #65 opened 2 years ago by hargoniX
  0