From cd7aeb7228a10a34ccf2a193215cd4ebff3a6da6 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sat, 14 Dec 2024 15:12:54 +0900 Subject: [PATCH] =?UTF-8?q?=E8=A8=B3=E6=B3=A8=E8=BF=BD=E8=A8=98?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/getting-to-know/functions-and-definitions.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 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 d70ebc5..f0fd29b 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 の使命の一部です。数学でも分野によって、数字をまったく異なる概念を表すのに使っています。このオーバーロードを可能にするための機能は、定義された名前をすべてその定義に置き換える前に、オーバーロードを探します。それが上のエラーメッセージを引き起こします。 [^fn1] @@ -224,4 +224,6 @@ Definitions that are to be unfolded are called _reducible_. Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand. Definitions produced with `abbrev` are marked as reducible. --> -舞台裏では、オーバーロードの解決時に、展開可能(unfoldable)であると内部でマークされる定義もあれば、そうでない定義もあります。展開される定義は *reducible* (簡約可能)と呼ばれます。Lean をスケールさせるためには、定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると、型が非常に大きくなり、機械が処理するのに時間がかかりますし、ユーザにとっても理解しづらいものになります。`abbrev` で生成された定義は reducible であるとマークされます。 \ No newline at end of file +舞台裏では、オーバーロードの解決時に、**展開可能**（unfoldable）であると内部でマークされる定義もあれば、そうでない定義もあります。展開される定義は**簡約可能**（reducible）と呼ばれます。Lean をスケールさせるためには、定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると、型が非常に大きくなり、機械が処理するのに時間がかかりますし、ユーザにとっても理解しづらいものになります。`abbrev` で生成された定義は reducible であるとマークされます。 + +[^fn1]: 訳注：この機能は[後の章](https://lean-ja.github.io/fp-lean-ja/type-classes/pos.html#%E6%95%B0%E5%80%A4%E3%83%AA%E3%83%86%E3%83%A9%E3%83%AB)で詳しく解説されます。