Hành vi không nhất quán của Coq liên quan đến các tham số ngầm định của định nghĩa Let

Question

Tôi đã tìm thấy một số loại hành vi không nhất quán của Coq liên quan đến các tham số ngầm định.

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. 

Các Let nét id1 dường như không làm cho t ngầm, trong khi đó khi bạn thay thế Let bởi Definition không có lỗi xảy ra. Tôi đã nhận được một cái gì đó sai hoặc là một lỗi này?

Answer 1

Tôi nghĩ đây là lỗi, vâng. Ký pháp để khai báo một đối số ngầm định đang bị bỏ qua trong trường hợp id1, như bạn có thể thấy với lệnh Print Implicit id1.