List.fold の記述の誤り

LeanByExample/Reference/Type/List.lean

@@ -111,10 +111,10 @@ class Foldl (α β : Type) where
 
 /-- #### List.foldl の使用例
 
-初期値が `init : α` で、適用する二項演算が `⊗ : α → β → α` だとする。
+デフォルト値が `init : α` で、適用する二項演算が `⊗ : α → β → α` だとする。
 また `⊗` は左結合的、つまり `a ⊗ b ⊗ c = (a ⊗ b) ⊗ c` であるとする。
 このとき `[b₁, b₂, b₃] : List β` に対して、
-`List.foldl` は左に初期値を挿入して順に `⊗` を適用したものに等しい。
+`List.foldl` は左にデフォルト値を挿入して順に `⊗` を適用したものに等しい。
 -/
 example [Foldl α β] {b₁ b₂ b₃ : β} (init : α) :
     [b₁, b₂, b₃].foldl (· ⊗ ·) init = init ⊗ b₁ ⊗ b₂ ⊗ b₃ := by
@@ -130,10 +130,10 @@ class Foldr (α β : Type) where
 
 /-- #### List.foldr の使用例
 
-初期値が `init : β` で、適用する二項演算が `⋄ : α → β → β` だとする。
+デフォルト値が `init : β` で、適用する二項演算が `⋄ : α → β → β` だとする。
 また `⋄` は右結合的、つまり `a ⋄ b ⋄ c = a ⋄ (b ⋄ c)` であるとする。
 このとき `[a₁, a₂, a₃] : List α` に対して、
-`List.foldr` は右に初期値を挿入して順に `⋄` を適用したものに等しい。
+`List.foldr` は右にデフォルト値を挿入して順に `⋄` を適用したものに等しい。
 -/
 example [Foldr α β] {a₁ a₂ a₃ : α} (init : β) :
     [a₁, a₂, a₃].foldr (· ⋄ ·) init = a₁ ⋄ a₂ ⋄ a₃ ⋄ init := by