假設有程式碼

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

這裡 id _ x 中的底線表示「省略的引數」，被稱為 hole，我們並沒有明確的給它任何值，比如 B。在展開這個 hole 時，我們用 meta variable ?0 替換它。但 meta variable 必須考慮 contextual variables 的 rigid form，因此進行套用得到 ?0 B x。這引發問題

什麼是 contextual variables？為什麼 contextual variables 是 B 與 x？ [tt-0009]

答案是，這些是 ?0 能看到且實際內容未知的變數，只能用 rigid form 替代

什麼是 rigid form？ [tt-000A]

rigid form 是 dependent type 中即使是 open term 也必須先進行計算而被迫在實作中出現的一種值；由於 meta variable 而被迫出現的值則叫做 flex form

現在我們手上有的 term 是 id (?0 B x) x，現在執行 id (?0 B x)，我們得到型別為

(x : (?0\ B\ \textcolor{red}{x})) \to (?0\ B\ \textcolor{red}{x})

的 term

\lambda x. x

注意到 $(x\ :\ (?0\ B\ \textcolor{red}{x}))$ 中兩個 $x$ 來源不同，不可混用，我用顏色表示它們的 scope 其實不同這件事

現在進入到把這個 term 套用到 x 上的環節了，因此觸發 $x\ :\ B$ 是否是 $?0\ B\ x$ 的 term 的合一計算，我們概念上紀錄成

?0\ B\ x \stackrel{?}{=} B

現在合一演算法必須找出合適的 $?0$ 來滿足等式。我們知道 $?0$ 應該是某種 lambda

\lambda 1. \lambda 2. \fbox{?}

，顯然 $\fbox{?} = 1$ 就會給出我們想要的答案，但這部分要怎麼做到？elaboration zoo 的演算法分成三個階段

Invert [tt-000B]

這裡的重點是，既然 $?0$ 已經套用了 $B$ 與 $x$ ，因此就創立關聯它所創立的 lambda 變數到其 contextual variables 的 map

1 -> B
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              2 -> x

現在右手邊的 term 只需要看自己的每個 rigid form 有沒有被指向，只要這個 map 裡面查找到有變數是指向 rigid form 自己即反過來創立 rigid form 指向新名字的 map

Rename [tt-000C]

因為我們右手邊的 term 是一個 rigid form $B$ ，因此 map 是

B -> 1

用第二個 map 去改寫右手邊 term $B$ 的內容，這樣我們就得到 $\fbox{?} = 1$

Lambda 化 [tt-000D]

最後進行 abstraction，就得到了

\lambda 1. \lambda 2. 1