chore: document `Lean.Elab.StructInst`, refactor · kmill/lean4@8d43b2e · GitHub

Commit

chore: document Lean.Elab.StructInst, refactor

Browse files

This PR does some mild refactoring of the `Lean.Elab.StructInst` module while adding documentation.

Documentation is drawn from @thorimur's leanprover#1928.

Loading branch information

kmill committed Nov 18, 2024

1 parent 405593e commit 8d43b2e