Skip to content

Issues: idris-lang/Idris2

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
22 Open 19 Closed
22 Open 19 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

Update error location when unexpectedly parsing binder error: bad message implem: parsing
#3454 opened Dec 21, 2024 by andrevidela
Update error messages for conflicting or redundant totality modifiers
#3442 opened Dec 11, 2024 by andrevidela
2
Proposal: Remove FC from Elab trees Feature request implem: interface elaboration
#3421 opened Nov 22, 2024 by andrevidela
2 tasks done
12
Improve error messages around usage of depends folder
#3411 opened Nov 11, 2024 by andrevidela
7
Investigate suspicious location tracking
#3409 opened Oct 30, 2024 by andrevidela
1
Properly report location of shadowed variable in warning error: bad message error: warning
#3408 opened Oct 30, 2024 by andrevidela
let binders in record Feature request
#3402 opened Oct 25, 2024 by andrevidela
2 tasks done
3
Conflicting fixity declaration in same file is not detected
#3389 opened Sep 20, 2024 by andrevidela
Parsing Performance & Maintainability.
#3369 opened Aug 9, 2024 by andrevidela
3 tasks
5
Syntax for Dictionary types Feature request
#3355 opened Jul 26, 2024 by andrevidela
2 tasks done
8
Remove = sugar for propositional Equality Feature request
#3211 opened Feb 6, 2024 by andrevidela
2 tasks done
3
typebind and autobind modifiers for operator fixity Feature request
#3113 opened Oct 21, 2023 by andrevidela
1 of 3 tasks
12
Make fixity declaration consistent with module syntax Feature request
#2998 opened Jun 9, 2023 by andrevidela
4 of 10 tasks
2
Document %transform documentation Improvements or additions to documentation language: transform
#2023 opened Oct 17, 2021 by andrevidela
4
Repl doesn't show the type of values after being evaluated cli: options cli: repl good first issue Good for newcomers
#1783 opened Jul 24, 2021 by andrevidela
1
[RFC] Access line, file and function name from the source discussion: design enhancement Feature request syntax
#1664 opened Jul 6, 2021 by andrevidela
1
Cannot reduce term in type signature when indexed implem: pattern-matching language: quantity status: confirmed bug Something isn't working
#1419 opened May 15, 2021 by andrevidela
5
Coverage checker gets confused in 0 context when indices are involved implem: pattern-matching language: quantity status: confirmed bug Something isn't working
#1417 opened May 15, 2021 by andrevidela
2
Performance improvement with compiling Nats and Fins? discussion: design Feature request implem: compilation implem: elaboration implem: unification
#1306 opened Apr 15, 2021 by andrevidela
1
Hide redundant arguments when pretty printing functions inside a parameters block enhancement error: bad message implem: pretty printing language: parameter blocks
#1214 opened Mar 20, 2021 by andrevidela
Test suite improvements Feature request library: test
#1185 opened Mar 14, 2021 by andrevidela
2 of 3 tasks
7
Reporting ill-indented multi-line strings enhancement error: reporting good first issue Good for newcomers
#1132 opened Feb 26, 2021 by andrevidela
ProTip! Adding no:label will show everything without a label.