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: Sep 13 2025 at 12:36 UTC