lean-ja / fp-lean-ja

Functional Programming in Lean の日本語訳. 演習問題への解答を含みます(作業中 🚧)
https://lean-ja.github.io/fp-lean-ja/
Other
7 stars 2 forks source link

1.3 functions... の翻訳を進める #1

Closed Seasawher closed 11 months ago

Seasawher commented 11 months ago

@aconite-ac @s-taiga @haruhisa-enomoto

相談なのですが,最後の段落のところの reducible (型が展開されるという性質のこと)は,どのように訳したものでしょうか

数学なら可約と訳すのが普通だと思いますが,型の話をしているときはどのように訳したものでしょうか?

Seasawher commented 11 months ago

ありがとうございます!