# Description


## Should this change go in the CHANGELOG?

<!-- Please delete this section if it doesn't apply -->
- [ ] If this is a fix, user-facing change, a compiler change, or a new paper
      implementation, I have updated [`CHANGELOG_NEXT.md`](https://github.com/idris-lang/Idris2/blob/main/CHANGELOG_NEXT.md) (and potentially also
      `CONTRIBUTORS.md`).