chore: refactor Elab.StructInst to use `mutual` for its `structure`s/`inductive`s

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

Closed kmill closed 6 days ago

kmill commented 6 days ago

Making use of #6125.

leanprover-community-bot commented 6 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e066c17a65f71a573bf074773d5012f3acfc4068 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-22 19:22:30)