You're right, there are several notable improvements in Idris2. I was mainly referring to the amount of code from the book that must be adapted. The QTT feature

You're right, there are several notable improvements in Idris2. I was mainly referring to the amount of code from the book that must be adapted. The QTT features, as you say, are opt-in; by default no new constraints are imposed.