RFC: in TC resolution, ← instantiateMVars (← inferType mvar)
is computed 2 or 3 times over for every new goal
#4284
Labels
closing soon
This issue will be closed soon (<1 month) as it is missing essential features.
RFC
Request for comments
Proposal
These three lines do this same computation:
lean4/src/Lean/Meta/SynthInstance.lean
Line 286 in f05a827
lean4/src/Lean/Meta/SynthInstance.lean
Line 243 in f05a827
lean4/src/Lean/Meta/SynthInstance.lean
Line 474 in f05a827
I propose to do it once, and pass this result as an argument to all these functions.
The text was updated successfully, but these errors were encountered: