simp_all は通るが simp at * は通らない例

[Seasawher]

simp_all は再帰的に単純化を繰り返している気がするので、再帰的でないといけない例をつくればよさそう…？

example (n : Nat) (P : Nat → Prop) (h1 : P (n + 0)) : P (n + 0 + 0) := by
  simp at *

  -- まだゴールが残っている
  show P n
  assumption

example (n : Nat) (P : Nat → Prop) (h1 : P (n + 0)) : P (n + 0 + 0) := by
  simp_all