Jon Sterling
Jon Sterling
As an update, I have experimented with this idea and I think it may be immortal. The only difficult thing (which is already an issue) is that we really need...
I experimented with this today, and fwiw the performance difference was negligible. But this might be affected by other parts of the design of the elaborator, which are changing rapidly....
It is probably doing so because it needs to bring it under many different restrictions. An alternative is to use `Value.act`, which we could try. (BTW the above is my...
I'm tagging this with "bug" because at least part of this issue indicates that there is broken code.
(/cc @freebroccolo, because he has more Agda experience than I do)
(One more remark that I'd say is, i don't think that careful controls on unfolding, opacity etc. are the solution here; these would be useful regardless, but I don't think...
Thank you! I'm curious to see if we can improve it :smile:
Hi @guillaumebrunerie, I've re-tested this example now and there is still an explosion, but it is generally much faster now. Here's the results on my laptop: ``` Defined test3 (0.021283s)....
@favonia Can you give a bit more detail about the level of generality you'd like to see?
The "true dominance" one is a great idea!