---
tags: violet
---
# sigma type

只能檢查不能推導，對應的 check case 是

check (.pair x y) (.sigma x a b) =>
  x <- check x a
  -- b 是 closure
  y <- check y (b.apply x)
  return .pair x y

- [x] parser 解析 pair 語法, e.g. `(1, 2)`
- [x] parser 解析 Sigma type 語法, e.g. `(x : Nat) ** Nat`
- [x] parser 解析 Product 語法 (non-dependent Sigma 的語法糖)
- [x] check 引入規則