28 lines
826 B
Text
28 lines
826 B
Text
#exit
|
|
|
|
example (x y : Nat) (h : x = y) : 0 + x = y + 0 := by
|
|
have := by exact h.symm
|
|
/-
|
|
Bad: we get "Goals accomplished" here
|
|
Should be:
|
|
... |- 0 + x = y + 0
|
|
-/
|
|
|
|
example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
|
|
constructor
|
|
· cases x
|
|
next => rfl --v Good: we get multiple states here as expected
|
|
next => repeat rw [Nat.zero_add] /- Good: we get the correct behavior here: Goals accomplished. -/
|
|
/-
|
|
Bad: We get "Goals accomplished" here
|
|
Should be:
|
|
... |- p
|
|
-/
|
|
|
|
example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
|
|
constructor
|
|
match x with
|
|
| 0 => rfl
|
|
| y+1 => repeat rw [Nat.zero_add] /- Good: We get the correct behavior here: Goals accomplished. -/
|
|
--^ Bad: get the `match` tactic initial state here.
|
|
-- Bad: we get "Goals accomplished" here
|