commit: 7dcb576acbbc2f522eee5bfcb99744070d446f53

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

Wed Jun 18 04:14:05 2025 +0900
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Jun 18 04:14:05 2025 +0900
tree: c4e3ec97c02bcaeb87f19f87763ccc6d2916732e
parent: 43aaae7348770036657845521d0451822df05946 [diff]

feat: proof-by-reflection support for converting semiring terms into ring ones

This PR implements the proof-by-reflection infrastructure for
embedding semiring terms as ring ones.

3 files changed

tree: c4e3ec97c02bcaeb87f19f87763ccc6d2916732e

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.