タイポ修正 (#90)

原文のジョークに合わせてリンク修正・訳注追記
lean-ja · Sep 14, 2024 · 29373c9 · 29373c9
1 parent 45d1ece
commit 29373c9
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/functional-programming-lean/src/dependent-types/pitfalls.md b/functional-programming-lean/src/dependent-types/pitfalls.md
@@ -319,7 +319,7 @@ Its pattern matching occurs on the _second_ argument, not the first argument, wh
 `Nat.add` in Lean's standard library is equivalent to `plusR`, not `plusL`, so attempting to use it in this definition results in precisely the same difficulties:
 -->
 
-このパターンマッチは第1引数ではなく **第二** 引数に対して行われるため、その位置に変数 `k` が存在すると簡約をすることができません。Leanの標準ライブラリにある `Nat.add` は `plusL` ではなく `plusR` と等価であるため、この定義で `Nat.add` を使おうとすると全く同じ問題が起こります：
+このパターンマッチは第1引数ではなく **第2** 引数に対して行われるため、その位置に変数 `k` が存在すると簡約をすることができません。Leanの標準ライブラリにある `Nat.add` は `plusL` ではなく `plusR` と等価であるため、この定義で `Nat.add` を使おうとすると全く同じ問題が起こります：
 
 ```lean
 {{#example_in Examples/DependentTypes/Pitfalls.lean appendR4}}

diff --git a/functional-programming-lean/src/next-steps.md b/functional-programming-lean/src/next-steps.md
@@ -36,7 +36,7 @@ Lean4そのものについては以下のリソースで記述されています
  * [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の拡張メカニズムの概要を提供しています。
- * [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) は再帰に関するジョークが好きな読者には面白いかもしれません。
+ * [Functional Programming in Lean](https://lean-ja.github.io/fp-lean-ja/) は再帰に関するジョークが好きな読者には面白いかもしれません。 [^fn3]
 
 <!--
 However, the best way to continue learning Lean is to start reading and writing code, consulting the documentation when you get stuck.
@@ -134,4 +134,6 @@ Disclaimer: the author of _Functional Programming in Lean_ is also an author of
 
 [^fn1]: 日本語訳は https://aconite-ac.github.io/theorem_proving_in_lean4_ja/
 
-[^fn2]: 原文が書かれた当時は `std4` という名前でしたが、改名されたことに合わせて日本語訳の文章を修正しています。
+[^fn2]: 原文が書かれた当時は `std4` という名前でしたが、改名されたことに合わせて日本語訳の文章を修正しています。
+
+[^fn3]: 非再帰版は https://leanprover.github.io/functional_programming_in_lean/