| attribute [-simp] Nat.left_eq_add -- This was later added to the simp set and interfere with the test. | |
| def foo : Nat := 0 | |
| def bar : Nat := 0 | |
| @[simp] theorem foo_eq_bar : foo = bar := rfl | |
| example : foo = bar := by simp [← foo_eq_bar] | |
| example : foo = bar + 1 := by | |
| simp [← foo_eq_bar] | |
| guard_target =ₛ foo = foo + 1 | |
| sorry | |
| def a : Nat := 0 | |
| def b : Nat := 0 | |
| def c : Nat := 0 | |
| @[simp] theorem abc : a = b ∧ a = c := And.intro rfl rfl | |
| example : a = b := by simp [← abc] | |
| example : a = c := by simp [← abc] | |
| example : a = c + 1 := by | |
| simp [← abc] | |
| guard_target =ₛ a = a + 1 | |
| sorry | |
| opaque d : Nat | |
| opaque e : Nat | |
| @[simp↓] theorem de : d = e := sorry | |
| example : d = e := by simp [← de] | |
| example : d = e := by simp [↓←de] | |
| example : d = e + 1 := by | |
| simp [↓←de] | |
| guard_target =ₛ d = d + 1 | |
| sorry |