Commit 2023-07-16 09:47 016138c2
View on Github →fix(tactic/linarith): instantiate metavariables in linarith (#19233) This probably isn't exhaustive, but catches the really trivial case. This doesn't appear to need forward-porting.
fix(tactic/linarith): instantiate metavariables in linarith (#19233) This probably isn't exhaustive, but catches the really trivial case. This doesn't appear to need forward-porting.