commit: 193f59aefeb1fd233656c811444bb014f94e8129

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

Sun Jun 01 13:46:49 2025 -0400
committer: GitHub <noreply@github.com>

Sun Jun 01 17:46:49 2025 +0000
tree: 9e392196cfaea379a22f54ed35f879b609174b49
parent: c681cccf1d0c2dc1d87a0963469be932f6884169 [diff]

feat: `grind +ring` by default (#8576)

This PR sets `ring := true` by default in `grind`. It also fixes a bug
in the reification procedure, and improves the term internalization in
the ring and cutsat modules.

10 files changed

tree: 9e392196cfaea379a22f54ed35f879b609174b49

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.