Commit 2024-02-12 10:30 35a3866a

View on Github →

chore(Util/SynthesizeUsing): Qq-ify (#9437) Most of the callers were already passing q() arguments anyway.

Estimated changes

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Util/SynthesizeUsing.lean

modified def synthesizeUsing'

modified def synthesizeUsing

modified def synthesizeUsingTactic'

modified def synthesizeUsingTactic