PR !4#11890: feat: the terminal refine linter

Stream: triage

[Random Issue Bot]

Today I chose PR #11890 for discussion!

feat: the terminal refine linter
Created by @damiano (@adomani) on 2024-04-04
Labels: awaiting-author, t-linter

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

[Damiano Testa]

This was a linter that would flag refine that closes a goal, suggesting to use exact instead.

Some experimentation with dubious benchmarking suggested that it caused slowdowns. I'm not planning on continuing this work, but if someone else is interested in taking over, feel free to do so!