search

stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
77 stars 18 forks source link

[ upstream ] Adapt to the idris-lang/Idris2#2604 #44

Closed buzden closed 2 years ago

buzden commented 2 years ago

Compiler's PR idris-lang/Idris2#2604 was merged with red CI because of elab-util, this should fix it.

buzden commented 2 years ago

BTW, @stefan-hoeck, I (as a day job user of elab-util and as a person who anyway has elab-util and sop installed and built locally) can volunteer myself as a person that can merge such upstream adaptations in cases when you are unavailable, say on a vacation or whatever (of course, if you trust me enough to give me such permissions).

stefan-hoeck commented 2 years ago

BTW, @stefan-hoeck, I (as a day job user of elab-util and as a person who anyway has elab-util and sop installed and built locally) can volunteer myself as a person that can merge such upstream adaptations in cases when you are unavailable, say on a vacation or whatever (of course, if you trust me enough to give me such permissions).

This is a great idea as, in fact, I'm sure you know far more about elab reflection in Idris than I do. You should receive an invitation by GitHub. Feel free to merge this whenever you think it is ready.