commit: 8e7dc7b3ecfd118251f61af1d6921524608d87f7

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

Wed Dec 24 15:46:53 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Dec 24 15:57:55 2025 -0800
tree: 5eabf51a697a77cf3da51d74b922979a9babdcbe
parent: e765138bb4dc05ed563237203c9db1ba81c2c57a [diff]

feat: add `AlphaShareBuilder`

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.