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.
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.idris only temporary. There's some discussion in the PR#2535 concerning whether the quantity annotation should be aMaybe Count. If that's what's going to happen in the end, then we should revert the implementation (but not the type) ofiCaseback toiCase = ICase EmptyFC.Don't merge this commit into main until #2535 is merged and incorproated into the nightly build.