feat: Implement `extends flat`

[eric-wieser]

This implements https://github.com/leanprover/lean4/issues/2666, allowing manual tweaking of whether structure inheritance is flat or nested, without forcing the user to fallback to the FlatHack approach in https://arxiv.org/abs/2306.00617.

This is documented via a docstring on the flat parser, which appear as a hover docstring as long as Lean/Parser/Command is imported.

Summary

Link to RFC or bug issue: #2666