-
Notifications
You must be signed in to change notification settings - Fork 375
Issues: idris-lang/Idris2
[ RFC ] Process for moving modules out of the
contrib package.
#2866
opened Jan 30, 2023 by
mattpolzin
Open
10
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Girards Paradox copied from Agda
language: universe levels
safety: proof of false
#3391
by yokto
was closed Sep 20, 2024
Unlawful This doesn't seem right
Monad implementation for Stream
library: base
status: invalid
#3383
by gallais
was closed Sep 13, 2024
Can't solve constraint between: or' z False and or' z False
status: invalid
This doesn't seem right
#3379
by johannes-riecken
was closed Sep 11, 2024
[ codegen ] Idris generates non-productive artifacts when optimizing
IO
#3375
by stefan-hoeck
was closed Aug 26, 2024
Searching of
auto inside pairs introduces ambiguity error between actually same things
implem: search
language: let
#3365
by buzden
was closed Aug 6, 2024
Test idris2/reflection/reflection024 fails due to not accounting for locales
Installation Issue
Problem compiling or running Idris
#3339
by elkcl
was closed Jul 2, 2024
Inconsistent error message when finding more than one implementation of an interface
#3313
by JavierGelatti
was closed Jun 17, 2024
Open
Data.Vect.nubBy for compile-time proofs
Feature request
#3285
by troiganto
was closed Jun 5, 2024
2 tasks done
[ preformance ] implementation of
unpack is inefficient
#3280
by stefan-hoeck
was closed May 24, 2024
A proof of Void
safety: proof of false
status: duplicate
This issue or pull request already exists
#3276
by petithug
was closed May 11, 2024
[ bug ] Buggy Something isn't working
Data.Fin.fromInteger in the presence of negative integer literals
safety: proof of false
status: confirmed bug
#3266
by stefan-hoeck
was closed Apr 22, 2024
Doc: "Multiplicities" section roadmap
admin: faq
documentation
Improvements or additions to documentation
#3264
by foxyseta
was closed Jun 20, 2024
Postfix functions are parsed as if inside unquote when are right after unquote
#3251
by buzden
was closed May 14, 2024
Regression in #3234, backticked infix operators are printed incorrectly
#3249
by buzden
was closed Apr 4, 2024
idris2 --init doesn't check a name of a package
cli: package init
status: confirmed bug
#3232
by DanMax03
was closed Jul 31, 2024
[ regression ]
Uninhabited (LTE 1 0) will no longer be found
#3230
by stefan-hoeck
was closed Mar 15, 2024
Source file "Main.idr" is not in the source directory when invoking compiler with
--source-dir
#3224
by phischu
was closed Mar 5, 2024
Failure to eliminate pattern case when matching by type
implem: pattern-matching
status: expected behaviour
#3218
by tauroid
was closed Feb 23, 2024
bash completion option is broken
Installation Issue
Problem compiling or running Idris
status: invalid
This doesn't seem right
#3144
by steveno
was closed Nov 16, 2023
Previous Next
ProTip!
Exclude everything labeled
bug with -label:bug.