add test

Author: JovanGerb

tests/lean/zetaDeltaFVarIdsLeakage.lean

@@ -0,0 +1,13 @@
+example : True := by
+  let a := 1
+  let b := 2
+  have : b = 2 := by simp [a,b]
+  have : a = 1 := by simp? [a]
+  have : 1 = 1 := by simp?
+  trivial
+
+example : False := by
+  let a := 1
+  let b := 1
+  have : a = 1 → False := sorry
+  simp (disch := simp [b]) [this, a]

tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out

@@ -0,0 +1,2 @@
+Try this: simp only [a]
+Try this: simp only