commit: 276193fc33b19ffd51f2519219c46c9476354998

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Sat Mar 29 16:09:18 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Mar 29 16:19:26 2025 -0700
tree: ed64f7c4996492e23a0272b4c1c2d80ecb189e32
parent: cde191da2621fc2cdbb8c959b0da34b2773ffc1d [diff]

fix: `abstractNestedProofs`

This PR fixes an issue in `abstractNestedProofs`.
We should abstract proofs occurring in the inferred proposition too.

src/Lean/Meta/AbstractNestedProofs.lean[diff]

1 file changed

tree: ed64f7c4996492e23a0272b4c1c2d80ecb189e32

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).