issues
search
leanprover
/
doc-gen4
Document Generator for Lean 4
Apache License 2.0
62
stars
41
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
feat: fix #166
#168
hargoniX
closed
9 months ago
0
feat: show the type of exists and fun arguments
#167
hargoniX
closed
9 months ago
0
Empty instances for
#166
nomeata
closed
9 months ago
1
De-indent comment block
#165
nomeata
opened
9 months ago
3
doc: Clearly spell out what happens on projects that fail to compile
#164
hargoniX
closed
9 months ago
0
Auto-generated lemmas appear before declaration
#163
alreadydone
opened
9 months ago
1
feat: docs below names
#162
hargoniX
closed
9 months ago
0
Put inductive/structure documentation before field documentation
#161
nomeata
closed
9 months ago
3
Show data fields only to avoid "not rendered due to size"
#160
alreadydone
opened
9 months ago
1
feat: use Kyle Miller's instance analysis algorithm
#159
hargoniX
closed
10 months ago
0
instances for vs instances mentioning
#158
hargoniX
closed
10 months ago
0
feat: html escape docstrings
#157
alexjbest
closed
10 months ago
4
Improve UX for long instance names
#156
utensil
opened
11 months ago
1
Lean statement not rendered for theorems defined as `def thm : Prop := statement`
#155
utensil
closed
11 months ago
0
feat: add jump-src.js for #src links
#154
digama0
closed
11 months ago
0
fix: don't fetch unused cache, FF fixes
#153
digama0
closed
11 months ago
0
feat: expand the current file in the navbar
#152
alexjbest
closed
11 months ago
1
feat: autolink references to files
#151
Ruben-VandeVelde
closed
11 months ago
3
Unclear error when running in a git repo without "origin" remote
#150
Ruben-VandeVelde
closed
11 months ago
1
[fix] wrong lean-toolchain version
#149
josojo
closed
12 months ago
0
Only linkify lean
#148
hargoniX
closed
12 months ago
0
Implement references / bibliography
#147
alexjbest
closed
1 month ago
7
Hyperlinking not working when an up-arrow occurs before the declaration name
#146
BoltonBailey
opened
1 year ago
0
fix: source links for Lake
#145
tydeu
closed
1 year ago
2
@[reducible] attributes are not shown
#144
alreadydone
closed
1 year ago
1
ERROR: could not execute external process 'cc'
#143
Seasawher
closed
1 year ago
2
error: no such file or directory
#142
Seasawher
closed
1 year ago
4
feat: include Lake as part of the core docs
#141
tydeu
closed
1 year ago
0
important type info is omitted
#140
alreadydone
closed
1 year ago
3
Recover information about arguments of structures that we extend from
#139
hargoniX
opened
1 year ago
0
chore: update toolchain
#138
semorrison
closed
1 year ago
1
Put field docstrings after the field
#137
eric-wieser
closed
1 year ago
1
Truncated docs page?
#136
alreadydone
closed
10 months ago
2
Generate hyperlinks for `library note [XYZ]` to the corresponding `library_note` doc-string.
#135
semorrison
opened
1 year ago
1
chore: update to new Lean/Lake version
#134
tydeu
closed
1 year ago
1
indexed DB invalidation
#133
hargoniX
opened
1 year ago
0
add dark mode
#132
4e554c4c
closed
1 year ago
3
Improve installation instructions
#131
DenisGorbachev
closed
1 year ago
0
feat: trigger search input when event handler is added
#130
alexjbest
closed
1 year ago
0
feat: don't copy .git folders in test
#129
alexjbest
closed
1 year ago
1
feat: list instances for defs also
#128
alexjbest
closed
1 year ago
2
Show documentation for built-in Quot stuff
#127
hargoniX
opened
1 year ago
0
Mangled docstring for `congrArg`
#126
chabulhwi
closed
2 months ago
2
fix: Use Z(separator) instead of S(ymbol) category
#125
hargoniX
closed
1 year ago
0
fix: properly comment out for the workaround
#124
hargoniX
closed
1 year ago
0
Mangled docstring for `CoeHTCT`
#123
eric-wieser
closed
1 year ago
2
Remove invalid comment
#122
eric-wieser
closed
1 year ago
3
fix: unicode dependency
#121
fgdorais
closed
1 year ago
0
feat: new CI setup
#120
hargoniX
closed
1 year ago
0
fix: correct character category testing
#119
fgdorais
closed
1 year ago
0
Previous
Next