chore: update test

2022-04-18 11:56:46 -07:00 · 2022-04-18 11:56:46 -07:00 · e69e469a37
commit e69e469a37
parent e6aee1e463
1 changed files with 6 additions and 1 deletions
--- a/tests/playground/sleep_save.lean
+++ b/tests/playground/sleep_save.lean
@ -29,4 +29,9 @@ example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 :
    save
    have : y = 0 := h₃ h
    simp [*]
-  | inl h => stop done
+  | inl h => stop
+    expensive_tactic
+    save
+    have : x = 0 := h₂ h
+    simp [*]
+    done