commit: ac0f699775a39fa6070135426c403fd5df204eda

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Mon Apr 22 01:27:44 2024 +0200
committer: GitHub <noreply@github.com>

Sun Apr 21 23:27:44 2024 +0000
tree: 38479b96dfe55635e4f56f7d67dc34035891a63d
parent: 69202d9b732501572e1a1ebdbcd617f93cd48472 [diff]

perf: improve heuristic at `isDefEq` (#3837)

This is intended to fail at present: it just adds a test case containing
a minimization of a Mathlib slowdown from #3807.

Prior to #3807, the declaration `exists_algHom_adjoin_of_splits'''` at
the end of the file would take around 16,000 heartbeats. Now it takes
around 210,000 heartbeats.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

src/Lean/Meta/ExprDefEq.lean[diff]
tests/lean/run/3807.lean[Added - diff]

2 files changed

tree: 38479b96dfe55635e4f56f7d67dc34035891a63d

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.