a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
30 lines
1 KiB
Text
30 lines
1 KiB
Text
set_option trace.Elab.info true
|
|
example (x y : Nat) (h : x = y) : 0 + x = y + 0 := by
|
|
have := by exact h.symm
|
|
--
|
|
--^ $/lean/plainGoal
|
|
-- Good: ..., this : y = x |- 0 + x = y + 0
|
|
|
|
example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
|
|
constructor
|
|
· cases x
|
|
next => rfl
|
|
-- Good: we get multiple states here as expected
|
|
--v $/lean/plainGoal
|
|
next => repeat rw [Nat.zero_add]
|
|
--^ $/lean/plainGoal
|
|
-- Bad? We still get all states except the one closed by implicit `rfl`
|
|
--^ $/lean/plainGoal
|
|
-- Good: ... |- p
|
|
|
|
example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
|
|
constructor
|
|
match x with
|
|
| 0 => rfl
|
|
-- Bad? We still get all states except the one closed by implicit `rfl`
|
|
--v $/lean/plainGoal
|
|
| y+1 => repeat rw [Nat.zero_add]
|
|
--^ $/lean/plainGoal
|
|
-- Good: we get the succ state here
|
|
--^ $/lean/plainGoal
|
|
-- Good: ... |- p
|