commit: 204d6d446bd6c52a889eb3645f61f51807f9f569

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

Mon Aug 04 08:11:01 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Aug 04 08:11:01 2025 -0700
tree: 55aab290f2113daf0483b4532225112ba947e237
parent: 78b941019b22af8cedab1f7fa4fd4041cb2c4daa [diff]

perf: `Expr.toPoly` in `grind`

This PR adds a version of `CommRing.Expr.toPoly` optimized for kernel
reduction. We use this function not only to implement `grind ring`,
but also to interface the ring module with `grind cutsat`.

2 files changed

tree: 55aab290f2113daf0483b4532225112ba947e237

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.