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

542 Open 643 Closed
542 Open 643 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

Interface which does not reference variable in body has error typechecking unless there is an implementation Feature request implem: meta freezing
#2813 opened Dec 11, 2022 by redfish64
1
linking behavior of record parameters names copied into values is confusing
#2812 opened Dec 10, 2022 by redfish64
6
Proof search fails sometimes in the presences of holes implem: search language: auto-implicit
#2801 opened Dec 7, 2022 by ohad
Pattern matching in a certain way causes a runtime error
#2790 opened Dec 5, 2022 by redfish64
1
Incorrect conversion checking of defined function admin: faq implem: unification
#2777 opened Nov 17, 2022 by ohad
3
Inconsistent behavior between :proofsearch and %search over a simple dependent pair
#2775 opened Nov 15, 2022 by ngeiswei
1
Variable use incorrectly inferred as W in L1 do-block language: do-notation library: linear
#2774 opened Nov 15, 2022 by CodingCellist
2
[ parser ] Bracket is not properly closed error is rendered to the last string in file. error: reporting good first issue Good for newcomers implem: parsing
#2771 opened Nov 12, 2022 by andorp
covering annotations do not apply to records
#2770 opened Nov 12, 2022 by Z-snails
IDE-mode reports wrong filename in warning (0.6.0)
#2763 opened Nov 7, 2022 by meraymond2
1
Able to cheat and use IO using Control.App without AppHasIO
#2760 opened Nov 7, 2022 by redfish64
1
when a data type without values is not public, the typechecker shouldn't be able to prove a value is impossible from another namespace
#2759 opened Nov 7, 2022 by redfish64
Machine readable compiler output. Feature request
#2740 opened Oct 31, 2022 by jfdm
%tcinline does not work if the function involves pattern matching
#2737 opened Oct 29, 2022 by Z-snails
4
Dotted expressions get in the way language: dot-patterns status: confirmed bug Something isn't working
#2726 opened Oct 21, 2022 by gallais
[ REPL ] search returns inappropriate result documentation Improvements or additions to documentation help wanted Extra attention is needed interactive: search status: expected behaviour
#2724 opened Oct 21, 2022 by ayaye
2
In REPL :psnext only works once
#2711 opened Oct 14, 2022 by ngeiswei
Type inference issue with test and the missing n. language: quantity status: expected behaviour
#2697 opened Oct 1, 2022 by thomasdziedzic
2
Proof of Void due to a coverage-checking bug safety: coverage safety: proof of false status: confirmed bug Something isn't working
#2690 opened Sep 28, 2022 by Russoul
Auto search cuts too early when an earlier auto variable is solved implem: elaboration implem: search language: auto-implicit
#2683 opened Sep 25, 2022 by ohad
1
Incomprensible type for hole interactive: bad message
#2679 opened Sep 23, 2022 by freddi301
All stdlib API docs to be found in the same place documentation Improvements or additions to documentation Feature request
#2672 opened Sep 21, 2022 by joelberkeley
JS backend: Performance degradation when using monad stack
#2670 opened Sep 20, 2022 by gergoerdi
3
Idris2 is anticlassical discussion: design
#2666 opened Sep 16, 2022 by gallais
1
Inconsistent coverage check with dependent pattern matching
#2663 opened Sep 15, 2022 by 0xd34df00d
ProTip! Type g i on any issue or pull request to go back to the issue listing page.