[arthur-adjedj]

This PR exists

Closes something, possibly

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 2429891 against f0fc2fc are in. No significant results found. @arthur-adjedj

• 🟥 build//instructions: +3.1G (+0.03%)

Medium changes (1✅)

• ✅ elab/stringLiteralDefEq//instructions: -1.4G (-1.30%)

Small changes (2✅, 5🟥)

• 🟥 elab/bv_decide_inequality//wall-clock: +78ms (+1.33%)
• 🟥 elab/bv_decide_realworld//wall-clock: +81ms (+3.70%)
• ✅ elab/stringLiteralDefEq//maxrss: -22MiB (-1.17%)
• and 4 hidden

[arthur-adjedj]

downstream

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#223.

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for e339883 against f0fc2fc are in. There are significant results. @arthur-adjedj

• 🟥 build//instructions: +2.6G (+0.03%)

Large changes (3✅)

• ✅ elab/stringLiteralDefEq//instructions: -1.4G (-1.25%)
• ✅ elab/stringLiteralDefEq//task-clock: -210ms (-2.38%)
• ✅ elab/stringLiteralDefEq//wall-clock: -208ms (-2.34%)

Small changes (5✅, 4🟥)

• ✅ compiled/async/select//task-clock: -12ms (-9.24%)
• ✅ compiled/async/select//wall-clock: -12ms (-8.67%)
• 🟥 elab/bv_decide_inequality//wall-clock: +68ms (+1.17%)
• ✅ elab/stringLiteralDefEq//maxrss: -20MiB (-1.06%)
• and 5 hidden