panic! と throw の違い

panic! はプログラムを止めないよ！

Lean で panic! マクロを使ったとき、

panic! "Something went wrong!"

って書くと「止まる」と思うかもしれないけど……実は止まらないの！

---

どうなるの？

• panic! は単にエラーメッセージを出すだけで、
• プログラムの実行はそのまま続いちゃうの。

たとえば Option.get! で none を強引に取り出しても、
panic! が呼ばれるだけで、「例外」にはならず、ただ default の値を返すだけなの。

これは、Lean の安全性（safe）を保つための設計なんだけど、
意図せず危険な動作を通してしまう可能性があるの。

---

たとえば：

def unsafeDiv (x y : Nat) : Nat :=
  if y == 0 then panic! "division by zero" else x / y

#eval unsafeDiv 10 0  -- => prints panic but returns 0

panic! が表示されるけど、プログラムはそのまま動いて
0（= Nat.default）が返ってきちゃうの。こわ〜い！

---

解決策は？

Lean の実行時に環境変数を設定することで、
本当に「パニックして止まる」ようにできるの：

LEAN_ABORT_ON_PANIC=1

でもこれは環境変数だから、ユーザー向けのアプリケーションなどでは
ちゃんと機能しないこともあるの。

---

じゃあどうしたらいいの？

安全のためには、

• panic! に頼らず、ちゃんと Except や Option のチェックを使う
• 本当に止めたいときは明示的に throw や IO.userError を使う

などを検討してね♪

No file, test, or entry point is named. First identify where this explanation belongs in the Lean-by-example documentation, then confirm the intended behavior and define the documentation change before starting; the issue does not currently state what completion should look like.