Basics: Coq 函数式编程 勘误讨论

[PhotonQuantum]

https://github.com/Coq-zh/SF-zh/blob/master/lf-current/Basics.v#L326

'构造子表达式'通过 将构造子应用到一个或多个构造子表达式 上构成。例如
[red]、[true]、[primary]、[primary red]、[red primary]、[red true]、
[primary (primary primary)] 等等

在原文中写的是

Constructor expressions are formed by applying constructors to zero or more constructor expressions.
E.g., red, true, primary, primary red, red primary, red true, primary (primary primary), etc.

这边是不是存在翻译上的偏差？因为我是初学者，所以对该怎么正确地理解和翻译也没个底🙈
个人感觉这句话的意思是说构造子可以是裸的，或者是可以将另一个构造子作为参数应用在这个新的构造子上？

[liyishuai]

我一时想不起有什么表达式不是构造子组成的。此处应为笔误，构造子后可以不接参数。

摘录教员笔记：

(BCP '19) After giving the lectures on this chapter in CIS500, I am a little concerned that it has gotten too technical. Toward the end, I found myself wanting to apologize for dumping too many details on them. Not sure what is the right fix, but for example the stuff I just added about "constructor expressions" may be a little too heavy. Ditto the lemmas from the standard library in the rewriting section, and the stuff about rewriting using quantified equalities. Thoughts from other instructors would be most appreciated.

MRC'20: IMO the "constructor expression" material gets a tad pedantic. Then again, in my context the students already know OCaml, so maybe I'm spoiled? Setting up that phrase and using it repeatedly suggests it's important and will come up in furture chapters, but it does not.

鉴于此段日后或将大改（我会建议英文版对constructor expression重新措辞），暂搁置术语译名，拟粗略译为：

构造子作用于参数，形成“构造子表达式”。其参数可以有零或若干个，这些参数皆为构造子表达式。

何如？

[PhotonQuantum]

这样翻译好理解不少，感谢释疑！

[liyishuai]

补充说明：表达式除了构造子作用于参数之外还包括：

• match ... with ...
• let ... in ...
• fix ...
• fun ... => ...
• 函数作用于参数

[OlingCat]

对，这里是笔误，稍后修复。