diff --git a/tests/playground/add_zeros.lean b/tests/playground/add_zeros.lean
new file mode 100644
index 0000000000..7803e94bf4
--- /dev/null
+++ b/tests/playground/add_zeros.lean
@@ -0,0 +1,20 @@
+def add (n m : Nat) : Nat := n + m
+@[simp] theorem addZero x : add 0 x = x := by
+  simp [add]
+
+syntax "bigAdd0Seq! " num : term
+
+macro_rules
+  | `(bigAdd0Seq! $n) =>
+    let n := n.toNat
+    if n == 0 then
+      `(0)
+    else
+      `(add 0 (bigAdd0Seq! $(Lean.quote (n - 1))))
+
+set_option maxRecDepth 10000
+
+theorem ex : bigAdd0Seq! 20 = 0 := by
+  simp
+
+#print ex
diff --git a/tests/playground/simp_binders.lean b/tests/playground/simp_binders.lean
new file mode 100644
index 0000000000..bf77039b2e
--- /dev/null
+++ b/tests/playground/simp_binders.lean
@@ -0,0 +1,27 @@
+axiom let_in {A B} (x : A) (f : A -> B) : B
+axiom add (x y : Nat) : Nat
+@[simp] axiom addZero (x : Nat) : add x 0 = x
+syntax "bigAdd0Seq! " num term:max : term
+syntax "bigAddSeq! "  num term:max : term
+
+macro_rules
+  | `(bigAdd0Seq! $n $acc) =>
+    let n := n.toNat
+    if n == 0 then
+      `(add $acc (add $acc 0))
+    else
+      `(let_in (add $acc (add $acc 0)) (fun acc' => bigAdd0Seq! $(Lean.quote (n - 1)) acc'))
+
+macro_rules
+  | `(bigAddSeq! $n $acc) =>
+    let n := n.toNat
+    if n == 0 then
+      `(add $acc $acc)
+    else
+      `(let_in (add $acc $acc) (fun acc' => bigAddSeq! $(Lean.quote (n - 1)) acc'))
+
+theorem ex1 (x : Nat) : bigAdd0Seq! 150 x = bigAddSeq! 150 x := by
+  simp
+
+-- theorem ex2 (x : Nat) : bigAddSeq! 5 x = bigAddSeq! 5 x := by
+--   simp