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

Idris requires type variables to be determined even when completely unused
#4511 opened Jul 9, 2018 by jasoncarr0
😕 1
Make versions of :t with differing degrees of normalization C-Low Hanging Fruit F-Discussion Z-Feature Request
#1170 opened May 2, 2014 by david-christiansen
Slices with left arguments allow only atomic expressions as that argument. A-Confirmed C-Moderate Effort S-Normal U-Parser
#524 opened Oct 9, 2013 by Melvar
1
All error messages should be reported using the IDEslave protocol C-Low Hanging Fruit S-Normal U-Editor Support U-Error Message
#879 opened Feb 12, 2014 by david-christiansen
@david-christiansen
7
Wrap record accessors in an implicit namespace C-Minor Effort U-Elaboration U-Language Design Z-Feature Request
#909 opened Feb 18, 2014 by david-christiansen
@david-christiansen
7
Add Read typeclass to standard library C-Low Hanging Fruit U-Library Design Z-Feature Request
#986 opened Mar 20, 2014 by jedesah
8
Difficult error message when mkForeign gets a non-literal name A-Confirmed F-Discussion S-Normal U-Error Message U-Foreign Function Interface
#1011 opened Mar 29, 2014 by joshvera
7
Executing main gives Prelude.undefined A-Confirmed C-Moderate Effort S-Normal U-Interactive
#1030 opened Apr 5, 2014 by puffnfresh
@david-christiansen
2
Confusing error message when mixing tabs and spaces for indentation in do blocks A-Confirmed C-Moderate Effort S-Normal U-Error Message U-Parser
#1082 opened Apr 18, 2014 by paulkoerbitz
2
Errors prevents loading C-Low Hanging Fruit Z-Feature Request
#1092 opened Apr 20, 2014 by puffnfresh
8
Make IdrisDoc namespace tracing strict C-Low Hanging Fruit U-Build System U-Documentation Z-Feature Request
#1099 opened Apr 22, 2014 by PhilipBorgesen
:missing improvements C-Low Hanging Fruit Z-Feature Request
#1111 opened Apr 24, 2014 by david-christiansen
1
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
fromList and exponential compile time S-Critical U-Type Checking Z-Optimisation
#172 opened Jan 30, 2013 by nicolabotta
8
Compile time Nats need to be optimised A-Confirmed S-Normal U-Type Checking Z-Optimisation
#1171 opened May 2, 2014 by UlfNorell
2
Unhelpful error when type inference fails in case blocks A-Confirmed S-Normal U-Error Message
#1217 opened May 10, 2014 by dfoxfranke
1
Consistent indentation with generated code? C-Low Hanging Fruit F-Discussion U-Documentation Z-Feature Request
#1227 opened May 14, 2014 by david-christiansen
4
Search for instances given a type C-Low Hanging Fruit U-Interactive Z-Feature Request
#1230 opened May 14, 2014 by LeifW
8
IDESlave support for :search C-Moderate Effort U-Editor Support Z-Feature Request
#1268 opened May 30, 2014 by david-christiansen
@david-christiansen
3
Provide a way to hide internal helper variables in proof mode C-Low Hanging Fruit S-Normal U-Interactive
#1301 opened Jun 9, 2014 by ahmadsalim
2
List available operators
#4923 opened Mar 1, 2023 by alexchandel
SOS : Subset or Sigma (or nothing the like) ? A-Confirmed C-Low Hanging Fruit S-Normal U-Error Message U-Pretty Printer
#1374 opened Jul 10, 2014 by nicolabotta
@david-christiansen
3
No Monoid for Ordering C-Low Hanging Fruit F-Discussion U-Library Design
#1378 opened Jul 11, 2014 by puffnfresh
1
Better error message when failing to parse "let" with nested "case" C-Low Hanging Fruit S-Normal U-Error Message U-Parser
#1402 opened Jul 17, 2014 by david-christiansen
5
Less than helpful error message when missing infix declaration for class members A-Confirmed C-Moderate Effort S-Normal U-Error Message U-Parser
#1167 opened May 2, 2014 by UlfNorell
ProTip! Adding no:label will show everything without a label.