From 29373c980994e1761923d1a4d5a264879d2041a5 Mon Sep 17 00:00:00 2001 From: s-taiga <56785231+s-taiga@users.noreply.github.com> Date: Sat, 14 Sep 2024 20:52:35 +0900 Subject: [PATCH] =?UTF-8?q?=E3=82=BF=E3=82=A4=E3=83=9D=E4=BF=AE=E6=AD=A3?= =?UTF-8?q?=20(#90)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 原文のジョークに合わせてリンク修正・訳注追記 --- functional-programming-lean/src/dependent-types/pitfalls.md | 2 +- functional-programming-lean/src/next-steps.md | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/functional-programming-lean/src/dependent-types/pitfalls.md b/functional-programming-lean/src/dependent-types/pitfalls.md index 2c5d189..6c69911 100644 --- 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 index eed2908..eb138dc 100644 --- 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]