coq - Let 定義の暗黙的なパラメーターに関する Coq の一貫性のない動作

Question

暗黙のパラメータに関して、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はないようですが、を置き換えてもエラーは発生しません。何か間違っているのでしょうか、それともバグですか?tLetDefinition

Answer 1

これはバグだと思います、はい。コマンドでわかるように、id1 の場合、暗黙の引数を宣言するための表記法は無視されていますPrint Implicit id1。