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
544 Open 648 Closed
544 Open 648 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

Add idris_crash_total function Feature request safety: totality status: discussion
#1691 by stepancheg was closed Jul 16, 2021
28
failure to recompile modules, seemingly randomly Installation Issue Problem compiling or running Idris status: confirmed bug Something isn't working
#2033 by attila-lendvai was closed Jan 21, 2022
1
24
JSON parser not working in repl
#791 by shmish111 was closed Nov 26, 2020
1
23
[PROPOSAL] Some syntax sugars Feature request
#1513 by glyh was closed Nov 24, 2021
20
RFC: Record syntax discussion: design Feature request language: record syntax
#626 by ziman was closed Feb 1, 2021
20
Feature requests and proposals Proposal
#13 by edwinb was closed Nov 25, 2021
20
JavaScript Backend: Ints are considered to be BigInts backend: javascript
#801 by DoctorRyner was closed May 10, 2021
19
One-line exception in REPL : "Exception: variable DataC-45Strings-fastUnpack is not bound" implem: compilation implem: scope status: confirmed bug Something isn't working
#1086 by algebraic-dev was closed Nov 28, 2021
17
Multiplicity subtyping with dependent types can break linearity implem: quantity subtyping status: confirmed bug Something isn't working
#73 by edwinb was closed Jan 12, 2021
1
16
Interface resolution bug library: contrib status: confirmed bug Something isn't working
#72 by edwinb was closed Jun 17, 2024
16
Unexpected run-time complexity performance
#16 by edwinb was closed Jun 14, 2021
1
16
Racket unsafe-fx functions missing in bootstrap/idris2_app/idris2.rkt backend: racket
#2279 by jfoutz was closed Sep 23, 2022
13
Local definitions in irrelevant definitions are incorrectly checked for relevance good first issue Good for newcomers language: quantity language: where status: confirmed bug Something isn't working
#55 by edwinb was closed May 25, 2021
@fabianhjr
13
JavaScript backend backend: javascript Feature request
#47 by edwinb was closed Jul 10, 2020
13
[ Nix, Racket, Termux, Install ] Idris2 cannot bootstrap properly on Arch Termux with Nix via Racket. backend: racket Installation Issue Problem compiling or running Idris os: nix
#1410 by alissa-tung was closed May 18, 2021
12
Syntax for complex numbers language: literals status: confirmed bug Something isn't working
#1200 by Atomotron was closed Mar 31, 2021
12
String interpolation for Idris2 Feature request implem: string syntax
#555 by andrevidela was closed Oct 18, 2021
3 tasks done
1
12
Equal Operator (=) treated as parsing error. status: discussion status: wontfix This will not be worked on syntax
#367 by jfdm was closed Nov 24, 2021
12
Test for not implemented feature is stuck rather than failing admin: continuous-integration
#264 by zenntenn was closed Jul 6, 2020
12
Nested with application rules aren't clearly defined
#261 by jinwoo was closed Jun 9, 2020
12
Projections out of a negative record are sometimes seen as total language: record projection language: record safety: positivity safety: proof of false safety: totality status: confirmed bug Something isn't working
#3030 by 91khr was closed Sep 8, 2023
1
11
Can't make directory. os: nix os: windows
#1524 by Kesanov was closed Nov 24, 2021
11
JavaScript Backend: Double's type is inferred incorrectly backend: javascript status: confirmed bug Something isn't working
#802 by DoctorRyner was closed Feb 6, 2021
11
"Can't infer type for case scrutinee" status: invalid This doesn't seem right
#764 by ulidtko was closed Feb 22, 2021
11
Implicits in Interface Functions cause Typecheck Error language: implicit status: confirmed bug Something isn't working
#67 by edwinb was closed Jan 20, 2021
1
11
ProTip! Follow long discussions with comments:>50.