commit: a86ca23ae3a8e9ed49a64236d78376290b2b093d

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

Fri Jul 10 17:56:04 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Fri Jul 10 17:56:04 2026 +0000
tree: e8e98b6713d49a3af907a17cf76143fb8149595b
parent: dd8e885bf12ec43c87046fd1484e29384d04ea6c [diff]

perf: fast path for `grind`'s internal envelope type `Ring.OfSemiring.Q type`

This PR implements a fast path for `grind`'s internal envelope type `Ring.OfSemiring.Q type`.

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean[diff]

1 file changed

tree: e8e98b6713d49a3af907a17cf76143fb8149595b

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.