commit: cba1892bf5ae6eefe6758ee5daebee221dcca97c

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

Sat Sep 06 17:53:41 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Sep 06 17:57:20 2025 -0700
tree: bd4f70a19815eb805bf512284782deef395306ae
parent: a31eb94e5afcbb5cc5f3ad00b72ecca6119a5027 [diff]

feat: improve `grind linarith` counterexamples for `NatModule`

This PR improves the counterexamples produced by `grind linarith` for
`NatModule`s. `grind` now hides occurrences of the auxiliary function
`Grind.IntModule.OfNatModule.toQ`.

3 files changed

tree: bd4f70a19815eb805bf512284782deef395306ae

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.