Jesper Cockx

I have mostly lost the motivation to investigate further why there are certain cases where the internal double-checker disagrees with the main checker. Since the flag itself has been implemented,...

@caryoscelus I'm sorry this is taking such a long time to get merged! Since it seems there are not many users/developers of the JS backend active here, I think it...

I'm honored that this repository serves as an example of how to build a backend but honestly it is just a side project that is currently on hiatus. I would...

- https://github.com/agda/agda/issues/426

Well how else would you handle parametrized modules? There is no such thing in Agda's internal syntax, so you need to desugar it to *something*.

I mean, yes, I was just answering the question "why was lambda lifting needed in the first place". Having some kind of let bindings and/or closures in internal syntax is...

@phikal this is great, please do not let it rot away!

This is a bit long ago so I don't really remember my actual use case :/ Still, shouldn't the behavior be the same in both cases, i.e. you should get...

Could you give a (preferably small) example of what exactly is broken? If there's a clear regression wrt 2.6.2, I believe we should prioritize this to still get a fix...

I think the fix that @nad proposes (adding `applyQuantityToContext zeroQuantity`) sounds reasonable for the TC primitives that just return something of type `Term` without otherwise modifying the TC state (`checkType`,...