test: for simp [x] where x is a let-variable

leanprover · Oct 25, 2023 · dbcc796 · dbcc796
1 parent a3642bd
commit dbcc796
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/tests/lean/run/letDeclSimp.lean b/tests/lean/run/letDeclSimp.lean
@@ -0,0 +1,12 @@
+example (a : Nat) : let n := 0; n + a = a := by
+  intro n
+  fail_if_success simp (config := { zeta := false })
+  simp (config := { zeta := false }) [n]
+
+example (a b : Nat) (h : a = b) : let n := 0; n + a = b := by
+  intro n
+  fail_if_success simp (config := { zeta := false })
+  trace_state
+  simp (config := { zeta := false }) [n]
+  trace_state
+  simp [h]