-
Notifications
You must be signed in to change notification settings - Fork 371
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
Statically enforce that all the logging options are documented
code: cleanup
documentation
Improvements or additions to documentation
good first issue
Good for newcomers
interactive: debug
#1124
opened Feb 25, 2021 by
gallais
Floats are inconsistent
language: float
safety: proof of false
status: confirmed bug
Something isn't working
#601
opened Aug 27, 2020 by
mr-infty
Racket cannot find libidris2_support on Mac M1
backend: racket
Installation Issue
Problem compiling or running Idris
os: mac
status: confirmed bug
Something isn't working
#1032
opened Feb 5, 2021 by
burcatowlet
Data.IOArray.newArray runtime exception with negative length
discussion: design
library: base
status: confirmed bug
Something isn't working
#885
opened Dec 29, 2020 by
Z-snails
contrib Data.Linear.Array is unsafe
discussion: design
library: contrib
#613
opened Aug 28, 2020 by
KyleDavidE
Allow expression evaluation in files similar to Lean4's #eval
Feature request
#2503
opened May 25, 2022 by
michaelmesser
2 tasks done
Pretty printing of duplicate names should avoid name clashes
error: bad message
naming
#35
opened May 20, 2020 by
edwinb
[Proposal] nix env script docker OR remove nix from the CI
admin: continuous-integration
Feature request
good first issue
Good for newcomers
help wanted
Extra attention is needed
os: nix
status: discussion
#1507
opened Jun 5, 2021 by
ohad
chez/chez014 test fails
Installation Issue
Problem compiling or running Idris
status: info needed
#860
opened Dec 18, 2020 by
kozross
Literate Idris Bird style
language: literate
status: wontfix
This will not be worked on
#788
opened Nov 23, 2020 by
nicolabotta
typebind
and autobind
modifiers for operator fixity
Feature request
#3113
opened Oct 21, 2023 by
andrevidela
1 of 3 tasks
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
Questions about string literal highlighting and hover
discussion: design
Feature request
ide: highlighting
#1543
opened Jun 12, 2021 by
michaelmesser
[ RFC ] Process for moving modules out of the
contrib
package.
Proposal
#2866
opened Jan 30, 2023 by
mattpolzin
Forced arguments don't propagate through the entire context
implem: unification
language: forced pattern
language: quantity
status: confirmed bug
Something isn't working
#1259
opened Apr 2, 2021 by
clayrat
Support type annotations on LHS of a monadic bind
<-
Feature request
#3327
opened Jun 21, 2024 by
joelberkeley
2 tasks done
Compiler failed to unify Type -> Type
implem: inference
implem: unification
status: expected behaviour
#2523
opened Jun 6, 2022 by
iacore
Unable to install Idris 2 with Home-brew on M1 MacBook (2021)
Installation Issue
Problem compiling or running Idris
status: info needed
#2404
opened Apr 6, 2022 by
Mithaecus
Allow trailing commas in the list syntax
Feature request
status: bikeshedding
Discussion, but on syntax
#2396
opened Apr 2, 2022 by
kuruczgy
2 tasks done
Previous Next
ProTip!
Exclude everything labeled
bug
with -label:bug.