commit: 7c950fc96c265807515062a2c319af032d108fc1

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

Sat Apr 18 23:00:47 2026 +0200
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Apr 18 23:00:47 2026 +0200
tree: 41a51d050a8b0f3d33721abe7aa68121d6714eed
parent: 91aa82da7f7c0d923ab0c0a76c5c2627d3fb70e5 [diff]

chore: minor tweaks to `Sym.simp` test and benchmark

This PR applies two minor tweaks:
- `tests/bench/sym/simp_1.lean`: share-common the proof term before
  counting objects in `getProofSize`, so the reported size reflects
  the shared representation.
- `tests/elab/sym_simp_3.lean`: use `>>` instead of `.andThen` when
  composing `Sym.Simp` methods.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

2 files changed

tree: 41a51d050a8b0f3d33721abe7aa68121d6714eed

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.