5 ms·
Yeah, 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 erro
by geckones 3mo ago
Yeah, 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.