Fix test

PatrickMassot · Sep 15, 2023 · 4305cd1 · 4305cd1
1 parent dfc5fb2
commit 4305cd1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/tests/lean/dsimpZetaIssue.lean b/tests/lean/dsimpZetaIssue.lean
@@ -4,10 +4,10 @@ example : let x := 0; x + 5 = 5 := by
   simp
 
 example : let x := 0; x + 5 = 5 := by
-  dsimp
+  dsimp (config := { zeta := true})
 
 example : let x := 0; x + y = y := by
-  dsimp
+  dsimp (config := { zeta := true})
   trace_state
   rw [Nat.zero_add]