commit: ca4322ff09910aa33c4f7d99aee36a7252219797

[log]
author: Cameron Zwarich <cameron@lean-fro.org>

Thu Aug 21 11:55:34 2025 -0700
committer: GitHub <noreply@github.com>

Thu Aug 21 18:55:34 2025 +0000
tree: abb669750c27be50e7eb21c4f1d0fe0e8cddbd0e
parent: d32f04ba211739f2c352fda3281bd1f067fbbf72 [diff]

fix: support `casesOn` for inductive predicates with computations on fields (#10023)

This PR adds support for correctly handling computations on fields in
`casesOn` for inductive predicates that support large elimination. In
any such predicate, the only relevant fields allowed are those that are
also used as an index, in which case we can find the supplied index and
use that term instead.

src/Lean/Compiler/LCNF/ToLCNF.lean[diff]
tests/lean/run/casesOnAcc.lean[Added - diff]

2 files changed

tree: abb669750c27be50e7eb21c4f1d0fe0e8cddbd0e

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.