commit: d63bebc76b349b8a83bccd97f8a9deafea236370

[log]
author: Joachim Breitner <mail@joachim-breitner.de>

Wed Nov 05 16:56:00 2025 +0100
committer: Joachim Breitner <mail@joachim-breitner.de>

Wed Nov 05 16:56:00 2025 +0100
tree: 645daa6931de446dc11b54254e86b35b2977d2be
parent: 3e86729ee0e11548a47f9b294d5292ada92c0b40 [diff]

perf: use hasIndepIndices

This PR makes use of `hasIndepIndices`. That function was unused since
commit 54f6517ca36b237b40e02aac62ea36dbd4179758, but it seems it should
be used.

src/Lean/Meta/Tactic/Cases.lean[diff]

1 file changed

tree: 645daa6931de446dc11b54254e86b35b2977d2be

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.