PR !4#13079: Lean pr testing 4152

Stream: triage

[Random Issue Bot]

Today I chose PR 13079 for discussion!

Lean pr testing 4152
Created by @None (@JovanGerb) on 2024-05-21
Labels: merge-conflict, new-contributor

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

I guess it can be closed, but we might really the instance caching behind it?

[Yaël Dillies]

cc @Jovan Gerbscheid

[Jovan Gerbscheid]

I closed the corresponding Lean4 PR, because I made a new one, but forgot to close the Mathlib PR.

For the instamce caching, I would say this is something we want, because of the performace benefits. But unfortunately the Lean developers aren't too keen on significant changes to the type class search implementation.