Skip to content

Issues: leanprover/verso

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

32 Open 27 Closed
32 Open 27 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

Nested lists shouldn't require non-list content
#225 opened Nov 13, 2024 by david-christiansen
Consistent use of CSS variables for themeing
#216 opened Nov 1, 2024 by david-christiansen
Print stylesheet: suppress "lozenges" for proof states highlighting Improvements or bugs related to highlighted Lean code
#215 opened Nov 1, 2024 by david-christiansen
Index improvement: group names by final namespace enhancement New feature or request Manual genre
#203 opened Oct 24, 2024 by david-christiansen
Manual genre: include "points of interest" in left-hand ToC
#187 opened Oct 18, 2024 by david-christiansen
Suggestion: special search for Lean code names?
#181 opened Oct 4, 2024 by mars0i
2
Disable hovers on docstring headers?
#175 opened Sep 23, 2024 by david-christiansen
Span of info is too small in rendered code
#151 opened Aug 30, 2024 by david-christiansen
*bubble* showing tactic state in custom notation
#146 opened Aug 19, 2024 by lecopivo
3
lean code block and variable command
#145 opened Aug 15, 2024 by lecopivo
1
open <namespace> command does not work as expected
#144 opened Aug 14, 2024 by lecopivo
Configurable proof state display
#137 opened Aug 8, 2024 by david-christiansen
Tests for LSP extensions
#136 opened Aug 8, 2024 by david-christiansen
Interleave Lean code with explanations enhancement New feature or request Manual genre
#135 opened Aug 8, 2024 by david-christiansen
error loading library, libleanmd4c.so
#132 opened Aug 1, 2024 by lecopivo
7
leanOutput Code action removes a `
#80 opened Apr 19, 2024 by nomeata
question: can we use verso by simply adding require verso to the lakefile?
#77 opened Apr 13, 2024 by Seasawher
1
multi-lang support
#76 opened Apr 13, 2024 by Seasawher
2
Confusing error message with include
#70 opened Apr 4, 2024 by PatrickMassot
Parser doesn't say "expected" always
#69 opened Apr 4, 2024 by david-christiansen
Go-to-def for {include A.B.C}
#68 opened Apr 4, 2024 by david-christiansen
Manual genre: multiple author rendering
#67 opened Apr 4, 2024 by david-christiansen
toggle displaying information
#66 opened Mar 22, 2024 by Seasawher
1
Support for multiline math formulas
#54 opened Mar 16, 2024 by utensil
7
Save Lean example contexts for later
#42 opened Feb 10, 2024 by david-christiansen
1
ProTip! Exclude everything labeled bug with -label:bug.