5

我发现 Coq 在隐式参数方面存在某种不一致的行为。

Section foo.
  Let id1 {t : Set} (x : t) := x.
  Let id2 {t : Set} (x : t) : t. assumption. Qed.
  Check id2 (1:nat).
  Check id1 (1:nat). (* Fails with "The term "1:nat" has type "nat" while it is expected to have type "Set"." *)
End foo.

Let定义id1似乎没有t隐含,而当您替换时Let不会Definition发生错误。我有什么问题还是这是一个错误?

4

1 回答 1

4

我认为这是一个错误,是的。在 id1 的情况下,声明隐式参数的符号被忽略,正如您在Print Implicit id1命令中看到的那样。

于 2011-11-15T20:23:35.087 回答