Skip to content

Issues: leanprover/lean4

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

348 Open 755 Closed
348 Open 755 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

Lake segmentation fault bug Something isn't working Lake Lake related issue
#2632 opened Oct 6, 2023 by yangky11
1 task done
5
compiler slowdown optimizing Option/List uses bug Something isn't working
#2631 opened Oct 6, 2023 by JamesGallicchio
1 task done
1
(kernel) unknown constant in mutually recursive definition bug Something isn't working
#2628 opened Oct 5, 2023 by nomeata
rfl runtime increases exponentially, causing timeout at 'whnf' bug Something isn't working
#2627 opened Oct 5, 2023 by collares
1 task done
1
Matching on a constructor that takes an instance argument using swift notation wrongfully tries to synthesize the instance bug Something isn't working
#2626 opened Oct 5, 2023 by felko
1 task done
RFC: built in option to suppress compilation of defs RFC Request for comments
#2619 opened Oct 3, 2023 by mattrobball
Slight change to typeclass use slows down 15 seconds -> 5 minutes awaiting-author Waiting for PR author to address issues performance A performance problem related issue or PR question Further information is requested
#2618 opened Oct 3, 2023 by philnguyen
1 task done
2
Strange error message from simp_arith bug Something isn't working
#2615 opened Oct 2, 2023 by david-christiansen
1 task done
(kernel) declaration has free variables error when extending class with typeclass parameter and extends bug Something isn't working
#2611 opened Oct 1, 2023 by SabrinaJewson
1 task done
2
RFC: add the option to add a prefix and a suffix to a doc-string when using inherit_doc low priority
#2622 opened Oct 1, 2023 by adomani
3
ident treated as token (e.g. str as a string) with behavior := symbol bug Something isn't working parser
#2608 opened Oct 1, 2023 by tydeu
1 task done
2
"compiler IR check failed" error when trying to create ToString instance bug Something isn't working
#2602 opened Sep 28, 2023 by stepchowfun
1 task done
1
lake clean should remove lakefile.olean in the root directory and under lake-packages Lake Lake related issue RFC Request for comments
#2592 opened Sep 26, 2023 by semorrison
3
Fields having inductive types with trivial structure are always stored boxed bug Something isn't working
#2589 opened Sep 26, 2023 by KislyjKisel
1 task done
1
Kernel error from dependent pattern match bug Something isn't working
#2588 opened Sep 26, 2023 by david-christiansen
1 task done
Unhelpful error message for mutual blocks with structures bug Something isn't working
#2587 opened Sep 26, 2023 by hargoniX
1 task done
Lake update across lake versions bug Something isn't working Lake Lake related issue
#2582 opened Sep 25, 2023 by PatrickMassot
1 task done
1
RFC: style: number of spaces before | RFC Request for comments
#2580 opened Sep 25, 2023 by mo271
2
Proposition fields result in defs not theorems bug Something isn't working
#2575 opened Sep 22, 2023 by eric-wieser
1 task done
Import error does not communicate file information enhancement New feature or request Lake Lake related issue
#2569 opened Sep 21, 2023 by BoltonBailey
1 task done
1
lake failing because of camel casing overriding user intentions bug Something isn't working Lake Lake related issue
#2567 opened Sep 20, 2023 by semorrison
match reduction is slow bug Something isn't working performance A performance problem related issue or PR
#2564 opened Sep 19, 2023 by kbuzzard
1 task done
1
1
isDefEq gets stuck on instantiated metavars bug Something isn't working
#2558 opened Sep 19, 2023 by arthur-adjedj
1 task done
Error: Unknown Free Variable from kernel local_ctx. bug Something isn't working
#2557 opened Sep 18, 2023 by bollu
1 task done
Unicode paths unsupported in Windows executables other than lean bug Something isn't working
#2554 opened Sep 18, 2023 by Kha
ProTip! Updated in the last three days: updated:>2023-10-03.