idris-lang/Idris2

Issues

• Proposal: Remove FC from Elab trees

  #3421 opened 5 days ago by andrevidela
  7

• System.Concurrency.channelGet is hard to use and too coupled into scheme support code

  #3424 opened 2 days ago by jarlah
  2

• Multiple evaluations of lazy values

  #3422 opened 5 days ago by spcfox
  2

• Improve error messages around usage of `depends` folder

  #3411 opened 15 days ago by andrevidela
  6

• Investigate suspicious location tracking

  #3409 opened a month ago by andrevidela
  1

• Cannot infer type after case in lazy lambda

  #3418 opened 7 days ago by spcfox
  1

• Inconsistent `%auto_lazy off` behavior

  #3416 opened 8 days ago by spcfox
  0

• Support implicit indexes in interfaces

  #3420 opened 6 days ago by spcfox
  0

• Slow typechecking interface with complex constraint

  #3419 opened 7 days ago by spcfox
  0

• Invalid FC of Pi-types

  #3417 opened 8 days ago by spcfox
  0

• Properly report location of shadowed variable in warning

  #3408 opened a month ago by andrevidela
  0

• A plea for improved Gambit support for bare metal

  #3387 opened 2 months ago by flintwinters
  9

• CLI flags interpreted as files if mistyped

  #3407 opened a month ago by eayus
  2

• Add new commands to repl `:show import` (to show already imported modules) and `:show loaded` (all available)

  #3410 opened 25 days ago by srghma
  0

• let binders in record

  #3402 opened a month ago by andrevidela
  3

• [inconsistency]: `--build` and `repl` need different $IDRIS2_PACKAGE_PATH

  #3404 opened a month ago by srghma
  2

• Generate only es6

  #3400 opened a month ago by srghma
  1

• Pattern matching 0 on numbers

  #3399 opened a month ago by maheshkronecker
  2

• Unable to `--exec` ambiguous mains

  #3398 opened 2 months ago by buzden
  0

• Typechecker complains that it can't match on erased argument when it actually can

  #3397 opened 2 months ago by buzden
  3

• Type checker silently stuck on missing import.

  #3390 opened 2 months ago by yellowsquid
  3

• Girards Paradox copied from Agda

  #3391 opened 2 months ago by yokto
  1

• Conflicting fixity declaration in same file is not detected

  #3389 opened 2 months ago by andrevidela
  0

• Unlawful `Monad` implementation for `Stream`

  #3383 opened 2 months ago by gallais
  1

• Can't solve constraint between: or' z False and or' z False

  #3379 opened 3 months ago by johannes-riecken
  3

• [ codegen ] Idris generates non-productive artifacts when optimizing `IO`

  #3375 opened 3 months ago by stefan-hoeck
  0

• Evaluation of partial functions during conversion

  #3372 opened 3 months ago by zanzix
  1

• Names received using as-matching are not reduced under `case`

  #3370 opened 3 months ago by buzden
  0

• Parsing Performance & Maintainability.

  #3369 opened 4 months ago by andrevidela
  4

• Holes at unerased quantity produce bad code

  #3367 opened 4 months ago by dunhamsteve
  0

• Searching of `auto` inside pairs introduces ambiguity error between actually same things

  #3365 opened 4 months ago by buzden
  3

• Case split causes my function to no longer be covering

  #3364 opened 4 months ago by FFFluoride
  4

• Syntax for Dictionary types

  #3355 opened 4 months ago by andrevidela
  7

• Regression in #3328, compilation now hangs sometimes

  #3354 opened 4 months ago by buzden
  2

• Erased type-casing function seen as total when it's not

  #3357 opened 4 months ago by gallais
  0

• Case split doesn't detect cases when working inside a namespace

  #3347 opened 5 months ago by JavierGelatti
  0

• Totality checker inconsistency when using Inf

  #3345 opened 5 months ago by JavierGelatti
  2

• Why quoted values are EmptyFC?

  #3344 opened 5 months ago by freddi301
  0

• Bootstrap with Racket error: `raco: Unrecognized command: exe`

  #3343 opened 5 months ago by barracuda156
  3

• Nested code blocks are ignored in literate markdown

  #3342 opened 5 months ago by joelberkeley
  1

• Test idris2/reflection/reflection024 fails due to not accounting for locales

  #3339 opened 5 months ago by elkcl
  0

• Incremental compilation includes some but not all metas

  #3337 opened 5 months ago by cypheon
  0

• Execution and compilation hangs indefintely

  #3309 opened 5 months ago by freddi301
  3

• Support type annotations on LHS of a monadic bind `<-`

  #3327 opened 5 months ago by joelberkeley
  9

• Reconstructing a (structurally smaller) aggregate from pattern-matched components trips up the totality checker

  #3317 opened 5 months ago by hyphenrf
  8

• Add error message with missing fixity namespace

  #3302 opened 5 months ago by andrevidela
  0

• Inconsistent error message when finding more than one implementation of an interface

  #3313 opened 5 months ago by JavierGelatti
  0

• Make output of ide-mode `:interpret` consistent to always return consistent datatype (String)

  #3311 opened 5 months ago by keram
  0

• Loading file in ide-mode changes working directory and causes errors on later actions

  #3310 opened 5 months ago by keram
  0

• unification failure between if then else statements when using isYes (decEq n a) as the condition

  #3300 opened 6 months ago by astaugaard
  2