Reorganize to submodule-per-toplevel-inductive-proof in Thm/Partial/Evaluation.lean

[cdisselkoen]

Category

Lean formalization

Describe the feature you'd like to request

Each toplevel theorem in Thm/Partial/Evaluation.lean should live in its own submodule (potentially with its own submodules Binary.lean, GetAttr.lean, etc). This allows some of these proofs to cleanly use the toplevel results from other ("earlier") proofs, unlike the current design, where that is impossible due to circular imports, and results in e.g. the h_spetv workaround in #368 (grep the code for h_spetv, and see also this comment thread on #368).

Describe alternatives you've considered

The current design, where some toplevel results are passed directly as arguments to "later" proofs.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change