Несогласованное поведение Coq относительно неявных параметров определений Let

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, по-видимому, не делает t неявным, тогда как при заменеLet по Definition ошибки не возникает.Я что-то не так понял или это ошибка?

Answer 1

Я думаю, что это ошибка, да.Нотация для объявления неявного аргумента игнорируется в случае id1, как вы можете видеть с помощью команды Print Implicit id1.