デフォルト値についてのコード例にコメントを追加する

Src/DefaultValue.lean

@@ -6,16 +6,21 @@ Python や PHP などの言語と同様に，Lean でも関数の引数にデフ
 たとえば，割り算で「分母がゼロのとき」への安全装置を実装した関数 `safeDiv` を定義してみましょう．複数のやり方がありますが，ここでは「分母がゼロでないという証明」を引数に取るようにしてみます．
 -/
 
+/-- 分母がゼロでないことを要求する割り算 -/
 def safeDiv (n m : Nat) (_h : m > 0) : Nat := n / m
 
+-- 分母がゼロでないことの証明を渡す必要がある
 #guard safeDiv 10 2 (by decide) = 5
 
-/- 当たり前のことですが，こうすると割り算を行うたびに毎回引数に証明を渡す必要が生じます．これでは面倒ですね．ここで，引数の証明項にデフォルト値を設定することができます．そうすれば，毎回証明を渡さなくても済みます．-/
+/- しかし, こうすると割り算を行うたびに毎回引数に証明を渡す必要が生じます．これでは面倒ですね．ここで，引数の証明項にデフォルト値を設定することができます．そうすれば，毎回証明を渡さなくても済みます．-/
 
+/-- 分母がゼロでないことを自動で証明しようとする割り算 -/
 def safeDiv' (n m : Nat) (_h : m > 0 := by decide) : Nat := n / m
 
+-- 分母がゼロでないことの証明を省略できる
 #guard safeDiv' 10 2 = 5
 
+-- 分母をゼロにするとエラー
 #check_failure safeDiv' 10 0
 
 /- デフォルト値を上書きするには，普通に値を渡せばよいです． -/