# elaboration

這裡完成的定義是基本 case 通過即可，對於更進階的自動安插 implicit 或是 pattern matching 展開等等不會在這裡處理

- [x] 定義 `Core.Term`
- [x] 定義 `Core.Val`
- [x] `Env.eval` 函數，簽名：`def Env.eval (env : Env) : Tm → Val`，表示在 `Env` 下執行 `Tm`
- [x] infer
- [x] check
- [x] unification [論文](https://dl.acm.org/doi/pdf/10.1145/3408983)
- [x] meta hole 語法
- [x] 為 implicit pi 生成 implicit lambda
- [x] 把 implicit 引數缺失轉換成 apply with hole 語法

## Paper

1. https://arxiv.org/pdf/2103.07397v1.pdf
2. http://www.cs.nott.ac.uk/~psztxa/publ/msfp08.pdf
3. https://arxiv.org/pdf/1601.05106.pdf
4. https://dl.acm.org/doi/pdf/10.1145/3158111

###### tags: `violet`