Daniel Mendler

There is some movement now, we may also see a fix in Company and upstream. Probably the fix won't be a proper fix for pcomplete which would be the ideal...

@danilevy1212 The eshell hotfix is not a great idea. I recommend to use the advices provided by my cape package. See https://github.com/minad/corfu#completing-in-the-eshell-or-shell. These advices fix the issues properly. I believe...

@danilevy1212 The cape dependency is pretty small, but you could also copy the definitions. plist comes from the pcase pattern matching.

@pard68 Which features of org-modern didn't work as expected for you? Note that you switch off every single one of the features.

@pard68 > the reason I have to turn it off the most is to edit heading levels. When editing heading levels I have no problems whatsoever and there shouldn't be...

Slim hasn't seen much maintenance recently, but I am interested in picking it up again, given that there is some support from the community. I've set up a sponsoring account,...

@AndrasKovacs It seems that the major difficulty is implementing inductive families. If those are not supported, eliminators and case-split are equally simple to implement. As far as I see, the...

> So I view it as a minimal version of pattern matching. I don't think it's difficult to add index unification on top of simple case splits, especially if we...

> MiniTT's splitting is via pattern matching lambdas. They're simpler IMO than Coq-style matching, where the matching is not tied to a lambda. Regarding pattern matching - I am confused....

> I don't think that's the case; I would actually even compress the pipeline a bit more, as Agda uses a separate scope-aware pass for operator parsing, and I'd instead...