grunweg
grunweg
> As for the TODO, I already have this, but its waiting on the q-expansion stuff thats coming. Should that still be a todo if its in the process of...
Let me label this with awaiting-review --- since I presume that, once the dependent PR is merged, you'd like a review :-) awaiting-review
Good point - let me rewrite this one in Lean instead. awaiting-author
In #13199, I have rewritten this linter: let me close this PR.
I wrote a test yesterday (of course!), but forgot to commit it :facepalm: I've updated it to use your example instance now (and added you as an author of the...
I just tried the logic you proposed. It works, so I switched to it (and added you an an author). I tweaked one test to consider nested syntax (which worked),...
Thanks for the fast review. bors r+
It looks like you have a merge conflict (which is why this PR does not appear in the review queue any more). Can you merge master, please? Thanks!