“Eval cbv delta in”在什么条件下展开Coq中的定义？

Question

在证明一般（有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 _.在类似情况下的作用。作为初学者，我知道潜伏着一种天真的误解。我错过了什么？

Answer 1

上丹尼尔的评论来扩展位，cbv delta将展开的标识符如果

1. 它具有主体（即，不是一个上下文变量，公理，字段中的模块参数当前模块函子，结合变量等），以及
2. 它是透明给予体，即，要么证明脚本与Defined而非Qed关闭或通过:=或自动义务战术（为Program Definition）或类型类的决议，定身（用于Instance s没有身体）和
3. 它没有被通过Opaque id或Strategy opaque [id]标记不透明的，并且
4. 它不是由“模块锁”另一恒定，即，一个模块（或模块仿函数）内定义与一个模块式归属经由:创建而不是<:（例外：如果模块类型本身提供身体为常数）

需要注意的是，目前，vm_compute可以得到约3（和统一引擎也可以，但compute，lazy，cbv， hnf，cbn（通常），simpl（通常）和red不能），但没有任何东西会绕过其他人。