我发现了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不会发生错误.我有什么不对或这是一个错误吗？
coq ×1