perf: bound expression comparisons in the type inference cache This PR fixes quadratic elaboration behavior for large string-literal equalities by limiting structural expression comparisons in the type inference cache.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.