我正在努力 软件基础 我现在正在做教会数字的练习。这是自然数的类型签名：
Definition nat := forall X : Type, (X -> X) -> X -> X.
我已经定义了一个函数 succ 类型 nat -> nat。我现在想定义一个这样的加法函数：
Definition plus (n m : nat) : nat := n nat succ m.
但是，我收到以下错误消息：
Error: Universe inconsistency.
这个错误信息实际意味着什么？
在Coq，一切都有类型。 Type 也不例外：如果你问Coq Check 命令，它会告诉你它的类型是...... Type！
实际上，这有点谎言。如果您通过发布指令要求更多详细信息 Set Printing Universes.，Coq会告诉你那个 Type 与第一个不同，但是“更大”。每个人都是正式的 Type 有一个与之关联的索引，称为Universe级别。通常在打印表达式时，此索引不可见。因此，该问题的正确答案是 Type_i 有类型 Type_j，对于任何索引 j > i。这需要确保Coq理论的一致性：如果只有一个 Type如果假设存在一组所有集合，那么就有可能表现出一种矛盾，类似于如何在集合理论中产生矛盾。
为了更容易使用类型索引，Coq为您提供了一些灵活性：没有类型实际上有与之关联的固定索引。相反，Coq每次编写时都会生成一个新的索引变量 Type，并跟踪内部约束，以确保它们可以使用满足理论要求的限制的具体值进行实例化。
您看到的错误消息意味着Coq的Universe级别约束求解器表示无法解决您要求的约束系统。问题是， forall 在定义中 nat 量化了 Type_i，但是Coq的逻辑力量 nat 本身就是一种类型 Type_j，与 j > i。另一方面，申请 n nat 要求 j <= i，导致一组不可满足的索引约束。