Skip to content

Issues: leanprover/reference-manual

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

74 Open 63 Closed
74 Open 63 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

Improve testing of Lake examples enhancement New feature or request
#273 opened Feb 3, 2025 by david-christiansen
Built-in operators and their precedence doc-request Request for missing documenation
#271 opened Feb 2, 2025 by eyelash
1
Why isn't a propositional computation rule for quotients enough to derive funext? doc-request Request for missing documenation
#267 opened Jan 30, 2025 by david-christiansen
Counterexamples for Lean's type system doc-request Request for missing documenation
#266 opened Jan 30, 2025 by TwoFX
Unify terminology around indexed families doc-request Request for missing documenation
#262 opened Jan 28, 2025 by david-christiansen
hard to distinguish text from code
#256 opened Jan 23, 2025 by joneugster
1
Document Lean's Language Server Functionalities doc-request Request for missing documenation
#255 opened Jan 17, 2025 by Julian
1
Clarify difference between SyntaxNodeKind and syntactic category doc-request Request for missing documenation
#242 opened Jan 10, 2025 by sgraf812
1
Subsubsubsection visibility.
#236 opened Jan 8, 2025 by nomeata
1
nested inductive types doc-request Request for missing documenation
#235 opened Jan 8, 2025 by nomeata
1
reflexive inductive types doc-request Request for missing documenation
#233 opened Jan 8, 2025 by nomeata
Explain the transformation rewrite attempts step by step doc-request Request for missing documenation
#232 opened Jan 8, 2025 by sgraf812
Mark Planned Content with a dagger already in the section title doc-request Request for missing documenation
#231 opened Jan 7, 2025 by nomeata
1
odd link anchor for “subsingletons”
#228 opened Jan 6, 2025 by nomeata
1
nested anonymous constructor syntax doc-request Request for missing documenation
#227 opened Jan 6, 2025 by nomeata
ui problem in lifting monad bug Something isn't working
#223 opened Dec 18, 2024 by lengyijun
1
Stack overflows on large Lean blocks
#211 opened Dec 14, 2024 by david-christiansen
Namespaces doc-request Request for missing documenation
#210 opened Dec 13, 2024 by david-christiansen
1
Specify the translation of match to auxiliary matcher functions doc-request Request for missing documenation low-priority Useful, but not currently a priority
#209 opened Dec 13, 2024 by david-christiansen
Reference Counting doc-request Request for missing documenation
#208 opened Dec 13, 2024 by david-christiansen
1
Ensure that all headers have permalinks enhancement New feature or request
#199 opened Dec 9, 2024 by david-christiansen
Document underscore separators in numeric literals doc-request Request for missing documenation
#197 opened Dec 9, 2024 by david-christiansen
All axioms break canonicity?
#188 opened Dec 7, 2024 by nielsvoss
1
Sigma doc-request Request for missing documenation
#176 opened Nov 28, 2024 by david-christiansen
Universe lifting doc-request Request for missing documenation
#174 opened Nov 28, 2024 by david-christiansen
ProTip! Adding no:label will show everything without a label.