Agda version that compiles this
ajrouvoet opened this issue · 1 comments
ajrouvoet commented
I tried with the development version of Agda of a while ago (014ea684be1f9c) and got compilation errors:
/home/arjen/projects/ataca.agda/src/Ataca/Core.agda:76,21-22
Generalizable variable Ataca.Utils.ℓ is not supported here
when scope checking ℓ
Would you mind sharing the version of Agda that works for you?
jespercockx commented
Currently it only works with my patched version of Agda that supports the runSpeculative primitive, which you can find here: https://github.com/jespercockx/agda/tree/runSpeculative?files=1