commit: 8cff74937a5a8a49e510403692682e5f7ac3b6b1

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

Sun Sep 27 18:39:48 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Sep 27 18:39:48 2026 +0000
tree: da0286f7305a7650ba7bcbf552dbf4dc48c724d2
parent: 6517561e4dc8d6ec3d69d18b703009f2279adfba [diff]

test: adjust 6467 for `Int.reduceNeg` no longer stripping `no_index`

`Int.reduceNeg` now leaves `-(no_index 2)` untouched, so `simp only [Int.reduceNeg]` correctly reports no progress.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

tests/elab/6467.lean[diff]

1 file changed

tree: da0286f7305a7650ba7bcbf552dbf4dc48c724d2

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.