commit: 96adf04a62fcbd48b7ddc51829b76bd161153c73

[log]
author: Kyle Miller <kmill31415@gmail.com>

Sat Sep 28 19:15:07 2024 -0700
committer: GitHub <noreply@github.com>

Sun Sep 29 02:15:07 2024 +0000
tree: 86421740d399f68d8372532a364cdeb7e646dec3
parent: 0db6daa8f125424f79b6a270d7c3777f7fb0f66e [diff]

fix: reduce parents in `structure` command (#5511)

Makes it possible to `extend` another structure through an abbreviation.
Also inserts a `withSynthesize` checkpoint for parents.

Closes #5417

src/Lean/Elab/Structure.lean[diff]
tests/lean/run/5417.lean[Added - diff]

2 files changed

tree: 86421740d399f68d8372532a364cdeb7e646dec3

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).