fix: use instantiateMVars before invoking pure function findIfToSplit

2022-02-23 16:25:33 -08:00 · 2022-02-23 16:25:33 -08:00 · 3e0ea7fbae
commit 3e0ea7fbae
parent a1366fcb3b
1 changed files with 1 additions and 0 deletions
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/src/Lean/Meta/Tactic/SplitIf.lean
@ -66,6 +66,7 @@ partial def findIfToSplit? (e : Expr) : Option Expr :=
    none

 def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do
+  let e ← instantiateMVars e
  if let some cond := findIfToSplit? e then
    let hName ← match hName? with
      | none       => mkFreshUserName `h