"Eval cbv delta in" 在什么情况下扩展 Coq 中的定义？
Under what conditions does "Eval cbv delta in" expand a definition in Coq?
在 Proof General（使用 Coq 8.5）中，我执行了以下操作：
Require Import Arith.
Eval cbv delta in Nat.add_comm 3 7.
输出为
Nat.add_comm 3 7 : 3 + 7 = 7 + 3
然而，Print Nat.add_comm. 给出了一个以两个 nats 作为输入的又长又复杂的函数。我希望我的代码能够扩展 Nat.add_comm 的定义，这正是 Eval cbv delta in _. 在类似情况下所做的。作为初学者，我知道潜藏着一种幼稚的误解。我错过了什么？
扩展一下 Daniel 的评论，cbv delta 将展开一个标识符 if
- 它有一个主体（即不是上下文变量、公理、当前模块函子的模块参数中的字段、绑定变量等），并且
- 它的正文是透明给出的，即证明脚本是用
Defined 而不是 Qed 关闭的，或者正文是通过 := 或自动义务策略（对于Program Definition) 或类型类解析（对于没有正文的 Instance），以及
- 它没有通过
Opaque id 或 Strategy opaque [id] 标记为不透明，并且
- 它不是由 "module-locking" 另一个常量创建的，即，通过
: 而不是 <: 在具有模块类型归属的模块（或模块仿函数）中定义（例外: 如果模块类型本身提供常量的主体)
请注意，目前 vm_compute 可以达到 3 左右（统一引擎也可以，但是 compute、lazy、cbv、hnf、cbn（通常）、simpl（通常）和 red 不能），但没有什么可以绕过其他人。
在 Proof General（使用 Coq 8.5）中，我执行了以下操作：
Require Import Arith.
Eval cbv delta in Nat.add_comm 3 7.
输出为
Nat.add_comm 3 7 : 3 + 7 = 7 + 3
然而，Print Nat.add_comm. 给出了一个以两个 nats 作为输入的又长又复杂的函数。我希望我的代码能够扩展 Nat.add_comm 的定义，这正是 Eval cbv delta in _. 在类似情况下所做的。作为初学者，我知道潜藏着一种幼稚的误解。我错过了什么？
扩展一下 Daniel 的评论，cbv delta 将展开一个标识符 if
- 它有一个主体（即不是上下文变量、公理、当前模块函子的模块参数中的字段、绑定变量等），并且
- 它的正文是透明给出的，即证明脚本是用
Defined而不是Qed关闭的，或者正文是通过:=或自动义务策略（对于Program Definition) 或类型类解析（对于没有正文的Instance），以及 - 它没有通过
Opaque id或Strategy opaque [id]标记为不透明，并且 - 它不是由 "module-locking" 另一个常量创建的，即，通过
:而不是<:在具有模块类型归属的模块（或模块仿函数）中定义（例外: 如果模块类型本身提供常量的主体)
请注意，目前 vm_compute 可以达到 3 左右（统一引擎也可以，但是 compute、lazy、cbv、hnf、cbn（通常）、simpl（通常）和 red 不能），但没有什么可以绕过其他人。