Andres Erbsen

I agree that recognizing a grammar as ambiguous is undecidable, I meant to ask about recognizing an input as ambiguous. Here is another way of asking mostly the same question:...

Thinking about it some more: it should be possible to detect that an input is ambiguous in O(n^2) time. This is because parsing an ambiguous input will finish in O(n^2)...

The current logging is indeed not very useful, but I think the main problem is that dename is simply not printing out the right information. I would rather not make...

I'm not sure whether you're following CoqPL, but I hear the new visual debugger comes down to 6 XML commands under the hood and it is intended to be supportable...

Same situation (or perhaps just slightly worse) for substituting let binders in the context: https://github.com/andres-erbsen/coq-experiments/blob/master/experiments/bench/subst_let.v

I spent a couple of hours reading though `evd.ml` and econstr code, and while I gained some understanding, I don't really see where the cubic behavior comes from. The flage...

lean seems only slightly superlinear on this benchmark (with the caveat the quality of the data is limited by lean's significant startup time and stack overflow tendencies) ~~~~~~ def foralln...

@ppedrot I am interested in discussing potential improvements on this issue (and #8237). I would hope that there is something that can be done here, but even if the conclusion...

Hmm. I don't know what else to ask for than `Ltac newintro mark := let H := fresh in intros H; mark H`. This would be used in the main...

I think we could batch a bunch of the introductions by first `change`ing the goal into a form where the binders are visible and then calling intros once. These binders...