目についた誤字修正

functional-programming-lean/src/getting-to-know/functions-and-definitions.md

@@ -184,7 +184,7 @@ When it makes sense to do so, natural number literals can be used for new types,
 This is part of Lean's mission of making it convenient to represent mathematics, and different branches of mathematics use number notation for very different purposes.
 The specific feature that allows this overloading does not replace all defined names with their definitions before looking for overloading, which is what leads to the error message above. -->
 
-このエラーは、Lean が数値リテラルのオーバーロード(overload)を許可しているために発生します。自然数リテラルは、あたかもその型がシステムに組み込まれているかのように、新しい型に使用することができます。これは、数学の表現を便利にするという Lean の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。
+このエラーは、Lean が数値リテラルの **オーバーロード**（overload）を許可しているために発生します。ある型に対して数値リテラルのオーバーロードを適切に設定することで、自然数リテラルはあたかもその型がシステムに組み込まれているかのように、新しい型に使用することができます。これは、数学の表現を便利にするという Lean の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。
 
 <!-- One way to work around this limitation is by providing the type `Nat` on the right-hand side of the definition, causing `Nat`'s overloading rules to be used for `38`: -->
 

functional-programming-lean/src/next-steps.md

@@ -35,7 +35,7 @@ Lean4そのものについては以下のリソースで記述されています
  * [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/) はLeanで証明を書くためのチュートリアルです。[^fn1]
  * [The Lean 4 Manual](https://leanprover.github.io/lean4/doc/) はLean言語とその機能のリファレンスを提供しています。本書執筆時点ではまだ不完全ですが、本書よりもLeanの多くの側面が詳細に記述されています。
  * [How To Prove It With Lean](https://djvelleman.github.io/HTPIwL/) は [_How To Prove It_](https://www.cambridge.org/highereducation/books/how-to-prove-it/6D2965D625C6836CD4A785A2C843B3DA#overview) という定評のある教科書のLeanベースの付録であり、紙と鉛筆で数学的証明を書くための入門書です。
- * [Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book) は中置演算子や記法などからマクロ・カスタムのタクティク・完全にカスタムな組み込み言語まで、Leanの拡張メカニズムの概要を提供しています。
+ * [Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book) は中置演算子や記法などからマクロ・カスタムのタクティク・完全にカスタムな組み込み言語まで、Leanの拡張メカニズムの概要を提供しています。 [^fn4]
  * [Functional Programming in Lean](https://lean-ja.github.io/fp-lean-ja/) は再帰に関するジョークが好きな読者には面白いかもしれません。 [^fn3]
 
 <!--
@@ -136,4 +136,6 @@ Disclaimer: the author of _Functional Programming in Lean_ is also an author of
 
 [^fn2]: 原文が書かれた当時は `std4` という名前でしたが、改名されたことに合わせて日本語訳の文章を修正しています。
 
-[^fn3]: 非再帰版は https://leanprover.github.io/functional_programming_in_lean/
+[^fn3]: 非再帰版は https://leanprover.github.io/functional_programming_in_lean/
+
+[^fn4]: 日本語訳は https://lean-ja.github.io/lean4-metaprogramming-book-ja/

functional-programming-lean/src/programs-proofs/arrays-termination.md

@@ -23,7 +23,7 @@ Arrays, however, have two drawbacks relative to lists:
  2. A loop that processes an entire array from left to right is a tail-recursive function, but it does not have an argument that decreases on each call.
 -->
 
- 1. 配列はパタンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために [証明の義務](../props-proofs-indexing.md) が課せられます。
+ 1. 配列はパターンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために [証明の義務](../props-proofs-indexing.md) が課せられます。
  2. 配列全体を左から右に処理するループは末尾再帰関数ですが、呼び出すたびに減少する引数を持ちません。
 
 <!--