commit: b0cd5e216ed401cd012e791990b2494dd0b8d41f

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

Tue Sep 09 20:37:20 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Sep 09 20:37:20 2025 -0700
tree: 13a18bde006250b8dedfdc4e0142605ca863dbe9
parent: c75d37f76bd5eca701dc67c1a19c8b7c50207712 [diff]

fix: unnecessary `NatModule`s in `grind linarith`

This PR fixes a performance issue in `grind linarith`. It was creating
unnecessary `NatModule`/`IntModule` structures for commutative rings
without an order. This kind of type should be handled by `grind ring` only.

2 files changed

tree: 13a18bde006250b8dedfdc4e0142605ca863dbe9

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.