idris2-elab-util
idris2-elab-util copied to clipboard
Published
20 hours ago •
stefan-hoeck
stefan-hoeck
Update reflection code to be compatible with Idris2#2535
Idris2#2535 adds a quantity argument to PCase and ICase. Update the reflection code to include this additional argument.
The fix in src/Language/Reflection/Syntax.idr is only temporary.
There's some discussion in the PR#2535 concerning whether the quantity
annotation should be a Maybe Count. If that's what's going to happen in the
end, then we should revert the implementation (but not the type) of iCase
back to iCase = ICase EmptyFC.
Don't merge this commit into main until #2535 is merged and incorproated into the nightly build.
