-
Notifications
You must be signed in to change notification settings - Fork 395
Pull requests: idris-lang/Idris2
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
[ fix #3670 ] Instantiate holes with correct PiInfo
language: interface
#3672
opened Nov 8, 2025 by
dunhamsteve
Loading…
[ fix #3669 ] Handle dotted in
findUsed
language: dot-patterns
language: with
#3671
opened Nov 7, 2025 by
spcfox
Loading…
2 tasks
[ refactor ] move parser into Idris
code: refactoring
implem: parsing
#3652
opened Oct 15, 2025 by
wizard7377
•
Draft
2 tasks done
[ Proposal ] Search only appropriate operator
language: fixity
status: discussion
#3650
opened Oct 6, 2025 by
buzden
Loading…
ideMode: Add failing test for incorrectly generated prefix when calling :make-case in a
.lidr file.
#3648
opened Sep 28, 2025 by
keram
Loading…
2 tasks
[ error ] fix FC of errors in with-applications
error: bad message
status: confirmed bug
Something isn't working
#3639
opened Sep 5, 2025 by
dunhamsteve
Loading…
[ fix ] harmonised the extension as expected in the PR request.
#3628
opened Aug 22, 2025 by
jfdm
Loading…
[ refactor ]
NameSet instead of List Name when possible
code: refactoring
#3613
opened Aug 13, 2025 by
gallais
Loading…
Make the property argument to
replace explicit
code: cleanup
library: prelude
#3531
opened Apr 11, 2025 by
joelberkeley
Loading…
1 task done
TDDwI: Minor changes to chapter10
doc: typedd
status: abandoned
status: discussion
#3433
opened Dec 3, 2024 by
sagehane
Loading…
fixed bugs that caused compiler to hang forever when there is %tcinline pragma
#3272
opened May 2, 2024 by
AntonPing
Loading…
ProTip!
no:milestone will show everything without a milestone.