commit: 723acce2a7179cd0f3ebb7deb833528cb6226fef

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

Wed Dec 24 16:05:03 2025 -0800
committer: GitHub <noreply@github.com>

Thu Dec 25 00:05:03 2025 +0000
tree: 5eabf51a697a77cf3da51d74b922979a9babdcbe
parent: e765138bb4dc05ed563237203c9db1ba81c2c57a [diff]

feat: add `AlphaShareBuilder` (#11793)

This PR adds functions for creating maximally shared terms from
maximally shared terms. It is more efficient than creating an expression
and then invoking `shareCommon`. We are going to use these functions for
implementing the symbolic simulation primitives.

src/Lean/Meta/Sym/Main.lean[diff]
src/Lean/Meta/Tactic/Grind.lean[diff]
src/Lean/Meta/Tactic/Grind/AlphaShareBuilder.lean[Added - diff]
tests/lean/run/grind_alphaShare_builder.lean[Added - diff]

4 files changed

tree: 5eabf51a697a77cf3da51d74b922979a9babdcbe

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.