@mcc maybe using https://idris2docs.sinyax.net/data/prelude/docs/Prelude.Interfaces.html#Prelude.Interfaces.for like for [1..8] (\i => ...)
(the list comprehension syntax is noted here https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#list-comprehensions although it's unclear whether the endpoints are inclusive lol)