Commit 2023-07-12 15:28 d3b54a9f
View on Github →fix(tactic/interval_cases): instantiate metavars (#19232) The test included in this commit fails without this change. This does not need forward-porting, the test already passes in Lean 4.
fix(tactic/interval_cases): instantiate metavars (#19232) The test included in this commit fails without this change. This does not need forward-porting, the test already passes in Lean 4.