From 40cc41f722f4e4a70946093d180e325554fa7f29 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sat, 14 Dec 2024 14:54:18 +0900 Subject: [PATCH] =?UTF-8?q?=E7=9B=AE=E3=81=AB=E3=81=A4=E3=81=84=E3=81=9F?= =?UTF-8?q?=E8=AA=A4=E5=AD=97=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/getting-to-know/functions-and-definitions.md | 2 +- functional-programming-lean/src/next-steps.md | 6 ++++-- .../src/programs-proofs/arrays-termination.md | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/functional-programming-lean/src/getting-to-know/functions-and-definitions.md b/functional-programming-lean/src/getting-to-know/functions-and-definitions.md index 8bddefa9..d70ebc59 100644 --- a/functional-programming-lean/src/getting-to-know/functions-and-definitions.md +++ b/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 の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。 diff --git a/functional-programming-lean/src/next-steps.md b/functional-programming-lean/src/next-steps.md index eb138dc5..4d2416de 100644 --- a/functional-programming-lean/src/next-steps.md +++ b/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] - 1. 配列はパタンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために [証明の義務](../props-proofs-indexing.md) が課せられます。 + 1. 配列はパターンマッチではなくインデックスによってアクセスされます。これにあたっては安全性を維持するために [証明の義務](../props-proofs-indexing.md) が課せられます。 2. 配列全体を左から右に処理するループは末尾再帰関数ですが、呼び出すたびに減少する引数を持ちません。