Reprint / Re-state Theorems

[jsimonrichard]

This is a simple answer to the discussion in #8.

Although it doesn't support conjunctive normal form, it integrates with the existing label system and can print multiple theorems that share a label.

Let me know what you think.

[sahasatvik]

I really like this setup! I've already implemented something in the v2.0.0 branch, and the result looks like this (output). It doesn't use labels like your solution though, which I would love to add.

v2.0.0 is a fairly big overhaul; you can check out the code here. I have also tried to use tidy to write a function reference: do let me know if things make sense there!

My solution stores every theorem in a big array (as a state), then retrieves them as necessary usingthm-restate or thm-display (after filtering). This is probably a little expensive, but it gives a lot of flexibility (like the list of theorems in this example). This is also geared more towards bulk restatement/display.

I'd like to integrate your solution into the restate/display setup, maybe something like thm-display(<thm>) fetches things with the label <thm>? That way, a <label> behaves like a special 'filter' function.

---

I also like the safeguard on thm-counters, I guess that prevents weird behaviour when nesting theorems?