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

Clear current search query, filters, and sorts
389 Open 624 Closed
389 Open 624 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

IO.FS.realPath doesn't resolve symbolic links (and junctions) on windows bug Something isn't working
#8507 opened May 28, 2025 by Rob23oba
1 of 3 tasks
Metavariables under binders can create terms that can become type incorrect after basic tactics bug Something isn't working
#8488 opened May 27, 2025 by kmill
3 tasks done
Metavariable suddenly appears from nowhere? bug Something isn't working
#8473 opened May 25, 2025 by lovely-error
4
rw selects the wrong equation, leading to impossible goals bug Something isn't working
#8454 opened May 23, 2025 by TwoFX
3 tasks done
2
FFI symbol lookup error in standalone Lean Files bug Something isn't working Lake Lake related issue
#8448 opened May 23, 2025 by abdoo8080
3 tasks done
@tydeu
apply duplicates goals bug Something isn't working
#8436 opened May 21, 2025 by sgraf812
3 tasks done
3
Hovering on syntax-less attributes shows no docstring bug Something isn't working
#8432 opened May 21, 2025 by nomeata
1
2
Unfortunate type inference failure bug Something isn't working
#8431 opened May 21, 2025 by hargoniX
3 tasks done
Closing bracket in auto-completion retains completion popup bug Something isn't working
#8430 opened May 21, 2025 by mhuisi
bug: projection on unsafeCast leads to "unknown free variable: _neutral" error/segfault bug Something isn't working depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it
#8407 opened May 19, 2025 by datokrat
3 tasks done
@zwarich
2
inductive in macro: invalid Name.append, both arguments have macro scopes, consider using eraseMacroScopes bug Something isn't working P-low We are not planning to work on this issue
#8381 opened May 16, 2025 by nomeata
1
Explicit ↑ can trigger slow unification bug Something isn't working
#8364 opened May 15, 2025 by MichaelStollBayreuth
3 tasks done
No dot completion for identifiers in most cases bug Something isn't working
#8353 opened May 15, 2025 by Rob23oba
3 tasks done
1
2
Coercion elaboration introduces monadic bind into non-monadic code, restricting universes bug Something isn't working P-medium We may work on this issue if we find the time
#8316 opened May 13, 2025 by TwoFX
3 tasks done
"unsupported pattern in syntax match" at wrong spot bug Something isn't working P-medium We may work on this issue if we find the time
#8304 opened May 12, 2025 by Happyves
simp/dsimp are not idempotent bug Something isn't working P-low We are not planning to work on this issue
#8300 opened May 12, 2025 by Timeroot
3 tasks done
4
split tactic introduces useless hypothesis bug Something isn't working P-low We are not planning to work on this issue
#8297 opened May 12, 2025 by TwoFX
3 tasks done
2
unfolding induction principle: incomplete reduction of matches bug Something isn't working P-medium We may work on this issue if we find the time
#8293 opened May 12, 2025 by nomeata
2
Using rcase/case tactic for recursive proofs when all arguments is variable cause an unexpected 'unknown identifier' error bug Something isn't working P-low We are not planning to work on this issue
#8282 opened May 11, 2025 by 7sDream
3 tasks done
2
Server crash using by decide bug Something isn't working P-low We are not planning to work on this issue
#8273 opened May 10, 2025 by franv314
3 tasks done
4
Creating an inductive type with a constructor called rec crashes Lean bug Something isn't working
#8258 opened May 8, 2025 by TwoFX
3 tasks done
1
Lake build should be runnable from subdirectory bug Something isn't working P-low We are not planning to work on this issue
#8248 opened May 6, 2025 by bollu
Spurious message "stuck at solving universe constraint" bug Something isn't working P-medium We may work on this issue if we find the time
#8247 opened May 6, 2025 by jeanas
3 tasks done
Stateful elaboration of mutual block causes 'unknown free variable' bug Something isn't working P-medium We may work on this issue if we find the time
#8223 opened May 4, 2025 by Vtec234
Parse issue involving try-catch-catch bug Something isn't working P-medium We may work on this issue if we find the time
#8220 opened May 4, 2025 by digama0
1
1
ProTip! Updated in the last three days: updated:>2025-05-25.