Commit 2025-11-03 00:36 27fa6806

feat(linarith): add linarith? mode which suggests a linarith only call (#28533) Adds linarith?, which traces the internal to watch which inequalities are being used, and suggests a linarith only call via the "try this:" mechanism. Also adds a +minimize flag, on by default, which then greedily tries to drop hypotheses from the used set, to see if the problem is still possible with a smaller set. Currently I don't have test case showing this is worthwhile, however. Contributions welcome.