安插隱式參數的方法 [tt-0008]

在最開始的程式碼

let id {A : U} (x : A) : A := x
let id2 {B : U} (x : B) : B := id _ x

裡面，其實 {} 中的綁定叫做隱式參數，這表示我們其實也可以用 id x 來調用該函數。但這時候要怎麼知道需要補一個 hole 進去呢？elaboration zoo 作者提出的簡易方案就是區分 implicit $\Pi$ type 與 implicit application，如此一來，當一個 implicit $\Pi$ type 被 explicit apply 的時候，我們就知道要安插 hole 了

以 id x 而言，如果要明確的用 implicit 調用它，就必須寫成 id {B} x，在語法就進行明確的區分。