From 58225c3f4e94de66a054e784eade5ce44b19371a Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 21 Oct 2023 23:46:10 +0900 Subject: [PATCH] =?UTF-8?q?=E5=8D=98=E8=AA=9E=E3=81=AE=E6=9C=80=E5=BE=8C?= =?UTF-8?q?=E3=81=AE=E9=95=B7=E9=9F=B3=E3=82=92=E5=8F=96=E3=82=8A=E9=99=A4?= =?UTF-8?q?=E3=81=8F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ユーザー → ユーザ --- .../src/getting-to-know/functions-and-definitions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 c2b86b9a..c51e6f05 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 @@ -224,4 +224,4 @@ 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 であるとマークされます． \ No newline at end of file