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

Type checker silently stuck on missing import. language: import scope: private scope: public status: expected behaviour
#3390 opened Sep 20, 2024 by yellowsquid updated Sep 25, 2024
3
A plea for improved Gambit support for bare metal Feature request
#3387 opened Sep 16, 2024 by flintwinters updated Sep 20, 2024
2 tasks done
6
Conflicting fixity declaration in same file is not detected
#3389 opened Sep 20, 2024 by andrevidela updated Sep 20, 2024
Evaluation of partial functions during conversion discussion: design implem: normalise
#3372 opened Aug 17, 2024 by zanzix updated Aug 18, 2024
1
Names received using as-matching are not reduced under case
#3370 opened Aug 13, 2024 by buzden updated Aug 13, 2024
Parsing Performance & Maintainability.
#3369 opened Aug 9, 2024 by andrevidela updated Aug 12, 2024
3 tasks
4
Holes at unerased quantity produce bad code
#3367 opened Aug 8, 2024 by dunhamsteve updated Aug 8, 2024
Known issues of the --mkdoc command backend: html good first issue Good for newcomers status: confirmed bug Something isn't working
#1918 opened Sep 12, 2021 by gallais updated Aug 6, 2024
4 of 6 tasks
2
Case split causes my function to no longer be covering
#3364 opened Aug 4, 2024 by FFFluoride updated Aug 5, 2024
4
Incorrect running times for Data.Seq due to missing laziness
#2867 opened Jan 30, 2023 by noinia updated Jul 31, 2024
6
Syntax for Dictionary types Feature request
#3355 opened Jul 26, 2024 by andrevidela updated Jul 26, 2024
2 tasks done
7
Regression in #3328, compilation now hangs sometimes
#3354 opened Jul 26, 2024 by buzden updated Jul 26, 2024
2
Erased type-casing function seen as total when it's not safety: coverage safety: proof of false status: confirmed bug Something isn't working
#3357 opened Jul 26, 2024 by gallais updated Jul 26, 2024
Layout processing - same column ; Haskell vs Idris good first issue Good for newcomers implem: parsing language: let syntax
#1201 opened Mar 17, 2021 by MilanKral updated Jul 26, 2024
2
Case split doesn't detect cases when working inside a namespace
#3347 opened Jul 7, 2024 by JavierGelatti updated Jul 7, 2024
Totality checker inconsistency when using Inf
#3345 opened Jul 7, 2024 by JavierGelatti updated Jul 7, 2024
2
Why quoted values are EmptyFC?
#3344 opened Jul 5, 2024 by freddi301 updated Jul 5, 2024
Bootstrap with Racket error: raco: Unrecognized command: exe Installation Issue Problem compiling or running Idris
#3343 opened Jul 5, 2024 by barracuda156 updated Jul 5, 2024
3
Nested code blocks are ignored in literate markdown
#3342 opened Jul 1, 2024 by joelberkeley updated Jul 4, 2024
1
Incremental compilation includes some but not all metas
#3337 opened Jun 30, 2024 by cypheon updated Jun 30, 2024
Definition with no RHS is incorrectly accepted as total implem: pattern-matching language: impossible safety: coverage safety: proof of false status: confirmed bug Something isn't working
#2250 opened Jan 5, 2022 by gallais updated Jun 23, 2024
11
Support type annotations on LHS of a monadic bind <- Feature request
#3327 opened Jun 21, 2024 by joelberkeley updated Jun 22, 2024
2 tasks done
9
Reconstructing a (structurally smaller) aggregate from pattern-matched components trips up the totality checker Feature request implem: termination checking
#3317 opened Jun 16, 2024 by hyphenrf updated Jun 22, 2024
8
total Omega : ⊥ implem: termination checking implem: typechecking language: data safety: positivity safety: proof of false status: confirmed bug Something isn't working
#1988 opened Oct 9, 2021 by yallop updated Jun 19, 2024
1
4
chez bootstrap requires large amount of memory Installation Issue Problem compiling or running Idris
#2994 opened Jun 1, 2023 by spocino updated Jun 18, 2024
8
ProTip! no:milestone will show everything without a milestone.