Stream: General

Topic: What to export from a development?


view this post on Zulip Gergely Buday (Aug 13 2025 at 10:16):

Naturally, you cannot tell in advance what other people would use from your proof development, but what is a good workflow for this?

You could set up simplification rules from good lemmas, make the main definitions and theorems, induction rules visible. What else?


Last updated: Aug 23 2025 at 01:39 UTC