4 ms·
Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.
by shiandow 4mo ago
Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.
- geckones 4mo agoYeah, I guess I can fix this easily by using qed instead of wip in the templates, but I have to check if the error messages will persist, I believe the qed error suppress the helpful messages now. But this does not scale, there is a lot of copy and paste when the proofs require case analysis, I want to check if I can emit edit comands to the editor in a sane way to automate that copy and pasting.