Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

match 文ではなくて式 #13

Open
Seasawher opened this issue Mar 31, 2024 · 1 comment
Open

match 文ではなくて式 #13

Seasawher opened this issue Mar 31, 2024 · 1 comment

Comments

@Seasawher
Copy link

Seasawher commented Mar 31, 2024

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/inductive_types.html#enumerated-types-%E5%88%97%E6%8C%99%E5%9E%8B

We will use the match expression to define a function from Weekday to the natural numbers:

Weekday から自然数への関数を定義するには、match 文を使うことができる:

@aconite-ac
Copy link
Owner

aconite-ac commented Aug 19, 2024

ご指摘ありがとうございます。
4章には "match statement" という記述も複数箇所あり、どちらに統一すべきか迷った覚えがあります。
FPiL と整合性を取るために全て「match 式」としてもよさそうですが、
現時点では原文準拠で "match statement" は「match 文」と、"match expression" は「match 式」と訳そうと思います。
メタプロの観点から match の構文上の分類が明確に理解でき次第、訳語の統一について再検討いたします。

追記:原文において "match statement" と "match expression" を区別する必要性がないように思われたため、「match 式」に訳語を統一いたします。いずれにせよ、再検討は実施する予定です。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants