我发现 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
发生错误。我有什么问题还是这是一个错误?