Skip to content

Issues: idris-lang/Idris-dev

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
691 Open 1,645 Closed
691 Open 1,645 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

The iPKG format should be replaced with a known configuration file format. C-Moderate Effort U-Package Management W-Refactoring Z-Feature Request
#1825 opened Jan 3, 2015 by jfdm
30
Able to prove two contradictory theorems
#4582 opened Nov 1, 2018 by Kazark
27
elab REPL: internal error: can't introduce here A-Confirmed C-Moderate Effort S-Normal U-Elaboration X-Elaborator Reflection
#2700 opened Oct 6, 2015 by cbiffle
27
Idris installation fails on Debian stable F-Question
#3350 opened Aug 8, 2016 by nicolabotta
23
Interface issues: a tentative summary F-Discussion U-Language Design U-Type Checking
#3114 opened Apr 13, 2016 by nicolabotta
20
Allow referencing previous constructors in half-positivity check A-Confirmed C-Moderate Effort S-Normal U-Totality Checking
#2803 opened Nov 9, 2015 by shlevy
19
Type mismatch due to lack of reduction of type defined in the same mutual block as target function. A-Confirmed C-Low Hanging Fruit S-Normal U-Error Message
#4229 opened Nov 28, 2017 by JadenGeller
17
Manipulation of Data.Bits generates large amount of code A-Confirmed C-Moderate Effort G-Intermediate Representation S-Normal U-Surprising Behaviour W-Debugging
#3842 opened Jun 1, 2017 by clayrat
17
Unexpected type checking behavior A-Confirmed F-Question U-Type Checking W-Debugging Z-Optimisation
#3509 opened Oct 31, 2016 by nicolabotta
17
Can't document a variable if it has the same name as one used in a nested type signature A-Confirmed C-Low Hanging Fruit S-Normal U-Documentation
#3419 opened Sep 11, 2016 by enolan
16
modifyIORef causes segmentation fault in FFI callback
#4391 opened Mar 22, 2018 by thalerjonathan
15
Overlapping implementations A-Confirmed C-Minor Effort F-Discussion U-Language Design Z-Feature Request
#4279 opened Jan 4, 2018 by nicolabotta
13
REPL evaluation does not reduce primitives called by a declared function A-Paper Cut C-Low Hanging Fruit S-Normal U-Interactive
#3995 opened Aug 14, 2017 by samestep
13
Module names should be required to match filenames. A-Confirmed C-Moderate Effort S-Normal U-Language Design
#2670 opened Sep 26, 2015 by cbiffle
13
Consolidate tests C-Low Hanging Fruit F-Meta S-Normal W-Refactoring
#2577 opened Sep 3, 2015 by edwinb
@steshaw @david-christiansen
13
Weird error message involving "Can't find implementation for" A-Confirmed C-Moderate Effort S-Normal U-Elaboration U-Error Message U-Type Checking W-Debugging
#4217 opened Nov 22, 2017 by michaelmesser
12
Type checking times again! A-Confirmed C-Moderate Effort S-Critical U-Type Checking Z-Optimisation
#3246 opened Jul 1, 2016 by nicolabotta
12
Mysterious type mismatch between @@constructors. Interfaces striking back again? C-Moderate Effort F-Discussion S-Normal U-Language Design
#3078 opened Mar 29, 2016 by nicolabotta
12
not cleaning all ibc files C-Low Hanging Fruit S-Normal U-Build System U-Package Management
#2710 opened Oct 8, 2015 by archaeron
12
Split the .ipkg commands and the HTML doc gen into separate executables C-Low Hanging Fruit F-Discussion U-Build System U-Documentation U-Package Management Z-Feature Request
#1126 opened Apr 29, 2014 by david-christiansen
12
Memory leaks in IDE server mode A-Confirmed C-Minor Effort S-Normal U-Editor Support U-Interactive W-Debugging
#4145 opened Oct 23, 2017 by clayrat
11
Incorrect pretty-printing of pruviloj-derived definition A-Confirmed C-Moderate Effort S-Normal U-Pretty Printer X-Elaborator Reflection
#3887 opened Jun 27, 2017 by RyanGlScott
11
Improve module resolution when encountering modules with the same name. C-Low Hanging Fruit F-Meta P-OS X S-Normal
#3539 opened Nov 30, 2016 by lehmacdj
11
Names do matter where they should not (broken alpha conversion) F-Question U-Error Message
#3449 opened Sep 22, 2016 by nicolabotta
11
Rewrite parser F-Request For Comment U-Parser W-Refactoring
#3443 opened Sep 19, 2016 by steshaw
1 of 4 tasks
11
ProTip! Updated in the last three days: updated:>2025-02-28.