[shiandow]

Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.

[geckones]

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.

[wizzwizz4]

Wouldn't it be better to improve the proof language so that copy-pasting is not necessary? (I know that's very hard, though.)

[geckones]

I improved the editor to allow auto-completion, and clicking on the errors almost always suggests a fix. wip -> qed always work. (: