You kid, but Idris2 documentation literally proposes almost this exact impl: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#note-declaration-order-and-mutual-blocks (it’s a bit facetious, of course, but still will work! the actual impl in the language is a lot more boring: https://github.com/idris-lang/Idris2/blob/main/libs/base/Data/Integral.idr)