aconite-ac / theorem_proving_in_lean4

Theorem Proving in Lean 4 日本語訳
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/
Apache License 2.0
10 stars 2 forks source link

match 文ではなくて式 #13

Open Seasawher opened 7 months ago

Seasawher commented 7 months ago

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 commented 2 months ago

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

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