commit: 974f9040d84942378b9c7524ee543522cdce816c

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

Mon Oct 26 09:29:18 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Oct 27 02:50:03 2026 +0000
tree: b9bebc0cdfc96666829c71ae2167b433ab8aa281
parent: a37796bb206431f8ccb063b457323903388ba198 [diff]

test: add `Sym.simp` arithmetic normalizer benchmarks

This PR adds benchmarks for the `arith` simproc of `Sym.simp`: long linear sums, polynomial expansions over `Int`, `Nat`, commutative (semi)rings and noncommutative rings, fields, rings with a nonzero characteristic, relations, and many small goals.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

tests/elab_bench/sym_arith_char.lean[Added - diff]
tests/elab_bench/sym_arith_expand.lean[Added - diff]
tests/elab_bench/sym_arith_field.lean[Added - diff]
tests/elab_bench/sym_arith_linear.lean[Added - diff]
tests/elab_bench/sym_arith_rel.lean[Added - diff]
tests/elab_bench/sym_arith_small.lean[Added - diff]

6 files changed

tree: b9bebc0cdfc96666829c71ae2167b433ab8aa281

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.