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

21 Open 13 Closed
21 Open 13 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

Small typo in README
#98 opened May 27, 2024 by chenson2018
1
1
Reduce size of generated HTML
#96 opened May 17, 2024 by david-christiansen
Check in CI that there's no import Lean checked in
#82 opened Apr 26, 2024 by david-christiansen
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
Add an example of a minimal genre
#74 opened Apr 5, 2024 by david-christiansen
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
5
Save Lean example contexts for later
#42 opened Feb 10, 2024 by david-christiansen
1
Generate RSS/Atom feeds Blog genre
#16 opened Jan 9, 2024 by david-christiansen
Support manually-specified token categories for fragments highlighting Improvements or bugs related to highlighted Lean code
#15 opened Jan 5, 2024 by david-christiansen
1
Generate self-contained HTML Manual genre
#12 opened Jan 3, 2024 by david-christiansen
Add a way to include an expression/proof with a given type, where the type doesn't show up in the text highlighting Improvements or bugs related to highlighted Lean code
#10 opened Dec 13, 2023 by david-christiansen
Add a way to specify scopes (global or local) of expressions highlighting Improvements or bugs related to highlighted Lean code
#9 opened Dec 13, 2023 by david-christiansen
lake script generate does not show build errors
#4 opened Dec 7, 2023 by nomeata
1
#exit not supported
#3 opened Dec 7, 2023 by nomeata
2
ProTip! What’s not been updated in a month: updated:<2024-05-10.