---
# System prepended metadata

title: Simpler indexed data type
tags: [violet]

---

---
tags: violet
---
# Simpler indexed data type

現在只有一些非常簡單的 data type 可以被定義，像是

```
data Nat
| zero
| suc Nat

data Bool
| true
| false
```

引入 simpler indexed data type 之後就會有

```
data Vec (n : Nat) (a : Type)
match n
| zero => nil
| suc n' => cons a (Vec n' a)
```

這需要更新 `dataTypeCtx` 這個欄位，讓它搜尋時要使用 `.rigid Vec` 的 spine，並對這個 partial pattern 進行 matching 來找到當前能使用的 pattern head
