[test] faster isDefEqApp

[datokrat]

No description provided.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 1332457 against a806b5c are in. There are significant results. @datokrat

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Runner for run build has different system configurations between commits.
• Runner for run other has different system configurations between commits.

• ✅ build//instructions: -48.3G (-0.43%)

Large changes (1✅)

• ✅ compiled/liasolver//instructions: -438.9M (-11.03%)

Medium changes (4✅)

• ✅ elab/big_match//instructions: -72.3M (-0.70%)
• ✅ elab/big_omega//instructions: -195.6M (-0.91%)
• ✅ elab/big_omega_MT//instructions: -201.9M (-0.93%)
• ✅ elab/bv_decide_large_aig//instructions: -794.5M (-2.00%)

Small changes (81✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 41fbc98 against d2f48db are in. No significant results found. @datokrat

• 🟥 build//instructions: +605.0M (+0.01%)

Small changes (1✅, 1🟥)

• ✅ compiled/server_startup//instructions: -16.8M (-4.48%)
• 🟥 elab/bv_decide_large_aig//task-clock: +120ms (+3.66%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-09 08:47:15)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d2f48db30713019241520218d0965227bbb64eed --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-09 09:24:27)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d2f48db30713019241520218d0965227bbb64eed --onto a806b5c9771998bcd75a5920da160b6d14a39346. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-09 09:24:25)
• ✅ Mathlib branch lean-pr-testing-13979 has successfully built against this PR. (2026-06-09 09:42:05) View Log